相关论文: Proof-checking Euclid
Theorem provers are important tools for people working in formal verification. There are a myriad of interactive systems available today, with varying features and approaches motivating their development. These design choices impact their…
First-order logic is the basis for many knowledge representation formalisms and methods. Providing technological support for learning to write first-order formulas for natural language specifications requires methods to test formulas for…
Elementary proofs of unique factorization in rings of arithmetic functions using a simple variant of Euclid's proof for the fundamental theorem of arithmetic.
In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal languages, aiming to offer our students a programming perspective on…
In this paper we develop cyclic proof systems for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions belong to the quantifier-free fragments…
This introduction begins with a section on fundamental notions of mathematical logic, including propositional logic, predicate or first-order logic, completeness, compactness, the L\"owenheim-Skolem theorem, Craig interpolation, Beth's…
Proof Blocks is a software tool that allows students to practice writing mathematical proofs by dragging and dropping lines instead of writing proofs from scratch. Proof Blocks offers the capability of assigning partial credit and providing…
The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an…
We present \textbf{QED}, an open-source multi-agent system that turns human-provided research questions into complete mathematical proofs without further human guidance. Its pipeline is designed to overcome common failures of single-query…
Paul Erdos claimed that mathematics is not yet ready to settle the 3x+1 conjecture. I agree, but very soon it will be! With the exponential growth of computer-generated mathematics, we (or rather our silicon brethrern) would have a shot at…
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to…
Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor…
We explore the relationship between Brouwer's intuitionistic mathematics and Euclidean geometry. Brouwer wrote a paper in 1949 called "The contradictority of elementary geometry". In that paper, he showed that a certain classical…
Euclidean geometry consists of straightedge-and-compass constructions and reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. We consider three versions of…
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…
We show how to generate and validate logical proofs of unsatisfiability from delta-complete decision procedures that rely on error-prone numerical algorithms. Solving this problem is important for ensuring correctness of the decision…
Despite significant developments in Proof Theory, surprisingly little attention has been devoted to the concept of proof verifier. In particular, the mathematical community may be interested in studying different types of proof verifiers…
Exploring selected reductio ad absurdum proofs in Book 1 of the Elements, we show they include figures that are not constructed. It is squarely at odds with Hartshorne's claim that "in Euclid's geometry, only those geometrical figures exist…
Elfe is an interactive system for teaching basic proof methods in discrete mathematics. The user inputs a mathematical text written in fair English which is converted to a special data-structure of first-order formulas. Certain proof…
Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast array of…