Related papers: Budge: a programming language and a theorem prover
A step-by-step presentation of the code for a small theorem prover introduces theorem-proving techniques. The programming language used is Standard ML. The prover operates on a sequent calculus formulation of first-order logic, which is…
We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational…
This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the…
Mechanical reasoning is a key area of research that lies at the crossroads of mathematical logic and artificial intelligence. The main aim to develop mechanical reasoning systems (also known as theorem provers) was to enable mathematicians…
This book can be seen either as a text on theorem proving that uses techniques from general algebra, or else as a text on general algebra illustrated and made concrete by practical exercises in theorem proving. The book considers several…
We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem…
The programming language Prolog makes declarative programming possible, at least to a substantial extent. Programs may be written and reasoned about in terms of their declarative semantics. All the advantages of declarative programming are…
Theorem proving in natural mathematical language - the mixture of symbolic and natural language used by humans - plays a central role in mathematical advances and education, and tests aspects of reasoning that are core to intelligence. Yet…
This dissertation discusses several problems loosely related, because they all involve a verification condition generator. The Boogie language is introduced; the architecture of a verification-generator is described. Then come more…
Logic programming is a declarative programming paradigm. Programming language Prolog makes logic programming possible, at least to a substantial extent. However the Prolog debugger works solely in terms of the operational semantics. So it…
This paper contains examples for a companion paper "The Prolog Debugger and Declarative Programming", which discusses (in)adequacy of the Prolog debugger for declarative programming. Logic programming is a declarative programming paradigm.…
We develop combinatorial test generation algorithms for progressively more powerful theorem provers, covering formula languages ranging from the implicational fragment of intuitionistic logic to full intuitionistic propositional logic. Our…
We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to…
A rather easy yet rigorous proof of a version of G\"odel's first incompleteness theorem is presented. The version is "each recursively enumerable theory of natural numbers with 0, 1, +, *, =, logical and, logical not, and the universal…
We describe a prototype theorem prover, UTP2, developed to match the style of hand-written proof work in the Unifying Theories of Programming semantical framework. This is based on alphabetised predicates in a 2nd-order logic, with a strong…
A classical result by Floyd ("On the non-existence of a phrase structure grammar for ALGOL 60", 1962) states that the complete syntax of any sensible programming language cannot be described by the ordinary kind of formal grammars…
Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using…
A logic program is an executable specification. For example, merge sort in pure Prolog is a logical formula, yet shows creditable performance on long linked lists. But such executable specifications are a compromise: the logic is distorted…
Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in…
To support reasoning about properties of programs operating with boolean values one needs theorem provers to be able to natively deal with the boolean sort. This way, program properties can be translated to first-order logic and theorem…