Related papers: Generic Automatic Proof Tools
This is the full version of a paper submitted to the Computability in Europe (CiE 2023) conference, with all proofs omitted there. In 2012 P. D. Azar and S. Micali introduced a new model of interactive proofs, called "Rational Interactive…
We present IntelliProof, an interactive system for analyzing argumentative essays through LLMs. IntelliProof structures an essay as an argumentation graph, where claims are represented as nodes, supporting evidence is attached as node…
We present the Theorem Prover Museum, and initiative to conserve -- and make publicly available -- the sources and source-related artefacts of automated reasoning systems. Theorem provers have been at the forefront of Artificial…
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary…
Ackermann's function can be expressed using an iterative algorithm, which essentially takes the form of a term rewriting system. Although the termination of this algorithm is far from obvious, its equivalence to the traditional recursive…
Following an early work of Dwork and Stockmeyer on interactive proof systems whose verifiers are two-way probabilistic finite automata, the authors initiated in 2004 a study on the computational power of quantum interactive proof systems…
Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we…
We report on our journey to develop ProofBuddy, a web application that is powered by a server-side instance of the proof assistant Isabelle, for the teaching and learning of proofs and proving. The journey started from an attempt to use…
We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error…
We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive proof assistants for…
We present a framework in Isabelle for verifying asymptotic time complexity of imperative programs. We build upon an extension of Imperative HOL and its separation logic to include running time. In addition to the basic arguments, our…
Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and…
We propose an approach for searching for counterexamples of statements about algebraic structures with a medium-sized signature using the Isabelle proof assistant in an efficient, parallel manner. We contribute a Python client Isabelle…
Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct…
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically…
The Isabelle/HOL proof assistant has a powerful library for continuous analysis, which provides the foundation for verification of hybrid systems. However, Isabelle lacks automated proof support for continuous artifacts, which means that…
Abella is an interactive system for reasoning about aspects of object languages that have been formally presented through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach to specification and…
This work proposes a complete algebraic model for classical information theory. As a precursor the essential probabilistic concepts have been defined and analyzed in the algebraic setting. Examples from probability and information theory…
We have developed a web-based pedagogical proof assistant, the Proof Tree Builder, that lets you apply rules upwards from the initial goal in sequent calculus and Hoare logic for a simple imperative language. We equipped our tool with a…
Formal verification of cyber-physical and robotic systems requires that we can accurately model physical quantities that exist in the real-world. The use of explicit units in such quantities can allow a higher degree of rigour, since we can…