Related papers: Developments in Formal Proofs
We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this problem but without…
Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a novel…
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further…
Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is,…
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have…
Formal proof checkers such as Coq are capable of validating proofs of correction of algorithms for finite field arithmetics but they require extensive training from potential users. The delayed solution of a triangular system over a finite…
Control systems are an integral part of almost every engineering and physical system and thus their accurate analysis is of utmost importance. Traditionally, control systems are analyzed using paper-and-pencil proof and computer simulation…
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on…
We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rules and is based on a frag- ment of first-order logic called…
In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctness of the content, allow computing with it, and produce…
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a…
This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and highly interactive setting for discussions around the…
Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning…
We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical…
The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wide range of other fields in mathematics. This paper presents…
In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations -- of which field operations are special cases-- on a representation of real numbers by…
Grover's algorithm relies on the superposition and interference of quantum mechanics, which is more efficient than classical computing in specific tasks such as searching an unsorted database. Due to the high complexity of quantum…
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms…
Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such…
In this paper we propose a new perspective on the evolution and history of the idea of mathematical proof. Proofs will be studied at three levels: syntactical, semantical and pragmatical. Computer-assisted proofs will be give a special…