A Mechanical Verification of the Independence of Tarski's Euclidean Axiom

<p>This thesis describes the mechanization of Tarski's axioms of plane geometry in the proof verification program Isabelle. The real Cartesian plane is mechanically verified to be a model of Tarski's axioms, thus verifying the consistency of the axiom system. The Klein–Beltrami model of the hyperbolic plane is also defined in Isabelle; in order to achieve this, the projective plane is defined and several theorems about it are proven. The Klein–Beltrami model is then shown in Isabelle to be a model of all of Tarski's axioms except his Euclidean axiom, thus mechanically verifying the independence of the Euclidean axiom — the primary goal of this project. For some of Tarski's axioms, only an insufficient or an inconvenient published proof was found for the theorem that states that the Klein–Beltrami model satisfies the axiom; in these cases, alternative proofs were devised and mechanically verified. These proofs are described in this thesis — most notably, the proof that the model satisfies the axiom of segment construction, and the proof that it satisfies the five-segments axiom. The proof that the model satisfies the upper 2-dimensional axiom also uses some of the lemmas that were used to prove that the model satisfies the five-segments axiom.</p>

A Mechanical Verification of the Independence of Tarski's Euclidean Axiom

<p>This thesis describes the mechanization of Tarski's axioms of plane geometry in the proof verification program Isabelle. The real Cartesian plane is mechanically verified to be a model of Tarski's axioms, thus verifying the consistency of the axiom system. The Klein–Beltrami model of the hyperbolic plane is also defined in Isabelle; in order to achieve this, the projective plane is defined and several theorems about it are proven. The Klein–Beltrami model is then shown in Isabelle to be a model of all of Tarski's axioms except his Euclidean axiom, thus mechanically verifying the independence of the Euclidean axiom — the primary goal of this project. For some of Tarski's axioms, only an insufficient or an inconvenient published proof was found for the theorem that states that the Klein–Beltrami model satisfies the axiom; in these cases, alternative proofs were devised and mechanically verified. These proofs are described in this thesis — most notably, the proof that the model satisfies the axiom of segment construction, and the proof that it satisfies the five-segments axiom. The proof that the model satisfies the upper 2-dimensional axiom also uses some of the lemmas that were used to prove that the model satisfies the five-segments axiom.</p>

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell’s containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library’s test suite, and interfaces from Coq’s standard library. Our work shows that it is feasible to verify mature, widely used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend hs-to-coq to handle partiality, and – since we found no bugs – attest to the superb quality of well-tested functional code.

Feasibility study of non-contact measurement in mechanical verification method for dissolution instrument

Dissolution instrument is an effective alternative method to study and evaluate the bioavailability of drugs in vitro, and an important means to ensure and evaluate whether the production technology and quality of solid oral preparations are reasonable and stable. It is found that the mechanical properties of the instrument will affect the determination of the drug, which will lead to the deviation of the determination results. Some methods of mechanical verification of dissolution instrument are analyzed and the application of non-contact measurement method is explored in mechanical verification. Experimental results show that the proposed non-contact measurement method has good measurement accuracy and repeatability.

About one method of evaluating the effectiveness of advertising text

The article considers the method of evaluating the effectiveness of the textual content of the advertising message. The basis of the proposed method is the linguistic principles, in which the effectiveness of the text is analyzed from the view of the decoding of information by the target recipient of the message. Materials used for the study were the texts used in SEO promotion of information resources, the method is based on the approach of breaking the text into keywords and phrases. The method of evaluating the effectiveness of the text is based on an analogue of the method of mechanical verification of the relevance of the text by the search engine, which was expanded by the parameters of expert evaluation of the quality of text construction.

Visualization of the Coated Electrode Welding

This work is dedicated to the evaluation of the welding process in terms of assessing the impact of weldability based on the recording of the non-destructive testing of the acoustic emission (AE). Measurements are performed utilising both materials with guaranteed weldability and materials with reduced weldability. In addition to welding, the thesis also discusses the material (metallographic and fractographic) and mechanical verification of joint formation and the variations in behaviour of metals of differing chemical composition. It also includes an analysis of AE records in relation to the condition of the material during the developing of fusion and resistance joints.

Visualization of Spot- welding Resistance

This contribution devotes to monitoring of processes running during joining of steel sheets by incadescent so called point welding using non-destructive trial method – acoustic emission (AE). The joining process is detailed described within experimental measuring from the point of view of metallurgic effects runnig during weld creation (records obtained by means of AE method). It takes into consideration quality of joined steels within welding data of steel producer. Steel welding (determined by chemical composition) during mechanical verification and firmness of welds consider results of measurement AE and fracture effect of point joints. The measurement also demonstrates conclusion about connection of metallurgic processes with material wave effects (AE measurement) and their impact on firmness of joint at steel with guaranteed welding, difficult welding and at their potential combination.