Academic literature on the topic 'Deduction and Theorem Proving'

Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project.<br>Bevis av säkerhetsegenskaper hos program genom formell verifiering kan göras med hjälp av interaktiva teorembevisare. Det program som skall verifieras representeras i en mellanliggande språkrepresentation inuti den interaktiva teorembevisaren, varefter påståenden kan konstrueras, som sedan bevisas. Detta är en process som kan automatiseras i hög grad. Här presenterar vi en metod för att effektivt skapa och bevisa ett teorem som visar sundheten hos den svagaste förutsättningen för att ett program avslutas framgångsrikt under ett givet postvillkor. Specifikt använder vi Poly/ML-implementationen av SML för att generera ett teorem i den interaktiva teorembevisaren HOL4 som beskriver egenskaper hos ett program i BIR, en abstrakt mellanrepresentation av maskinkod som används i PROSPER-projektet.

Depuis les travaux de Martelli et Montanari en 1982, la resolution de problemes de E-unification s'effectue souvent par transformation de systemes d'equations. L'objectif de cette these est de presenter des nouvelles regles de transformations qui de- crivent de facon unifiee comment appliquer des axiomes a la ra- cine des termes. Les proprietes theoriques de ces regles sont etablies (correction, completude. . . ). Nous prouvons egalement que cette approche, basee sur la notion de presentations strictement resolventes, est plus generale que des algorithmes tres connus (Root-Rewriting [J. Gallier &amp; W. Snyder ], Mutation Syntaxique [C. Kirchner ]). Une analyse du comportement de ces regles per- met d'etablir l'inter^et de l'application d'axiomes a la racine et de definir le type de presentations strictement resolventes qui devraient fournir les meilleurs resultats. Ces presentations sont generees automatiquement. Pour ce faire, nous introduisons la notion de completion strictement resolvente. Elle permet de definir les proprietes theoriques des regles de completion donnees. Differentes strategies sont etu- diees, allant d'une strategie qui termine toujours a la strategie (parfois divergente) conduisant a une presentation tres efficace. Des recherches theoriques peuvent s'effectuer dans ce (nouveau) formalisme general. Elles s'appliquent aux algorithmes subsumes par cette approche. Par exemple, les avantages vis a vis du parallelisme sont etablis et conduisent a une presentation compacte de l'ensemble des unificateurs. Des optimisations theoriques plus complexes sont egalement etudiees. La detection des instanciations inutiles des variables lors de l'unification d'un terme avec les t^etes de regles est la plus importante. Elle permet d'etablir la completude des solutions donnees pour un probleme m^eme si la presentation n'est pas strictement resol- vente (completion divergente). Les resultats experimentaux mettent en valeur la simplicite et la generalite de cette nouvelle approche. Sa generalite permet egalement de comparer les differents algorithmes et de justifier l'utilisation de la strategie non complete de generation des re- gles. L'etude de cas particuliers montre que l'on peut ainsi ob- tenir des resultats tres interessants en un temps tout a fait raisonnable. On peut donc envisager d'utiliser ce module de E- unification au sein d'un demonstrateur<br>Since Martelli and Montanari's work in 1982, E-unification problems are often considered are set of equations. This thesis presents new transformation rules which describe application of axioms at the root of the terms. The theoretical properties are established (soundness, completeness,. . . ). We also prove that this approach, based on strictly resolvent presentations, is more general than well known algorithms (Root-Rewriting [J. Gallier &amp; W. Snyder], Syntactic mutation [C. Kirchner]). The analysis of the behavior of these rules proves the interest of the applica- tion of axioms at the root and suggests which strictly resolvent presentations should give the best results. These presentations are generated automatically. The theoreti- cal properties of the given completion rules are proved thanks to the notion of strictly resolvent completion. Different strategies are studied, going from a terminating strategy to a (potentially divergent) strategy resulting in very efficient presentations. Theoretical researches can be done in this (new) general frame- work. They apply to the subsumed algorithms. For instance, paral- lelism is studied and leads to a compact presentation of the com- puted unifiers. Other more complex optimisations are also stu- died. The detection of useless instanciations while unifying with the left hand-side of a rule is the most important. It is useful to prove the completeness of the solution found for a given prob- lem when the presentation is not strictly resolvent (divergent completion). Experimental results show the simplicity and the generality of this new approach. Its generality allows comparison with other well-known algorithms and justifies the usefulness of the diver- gent strategy. The study of particular cases proves that it leads to very interesting results in a reasonable time. Thus, this E- unification procedure can be used in a theorem prover

Le model checking est une technique de vérification automatique de propriétés de correction de systèmes finis. Normalement, les outils de model checking ont deux caractéristiques remarquables : ils sont automatisés et ils produisent un contre-exemple si le système ne satisfait pas la propriété. La Déduction Modulo est une reformulation de la logique des prédicats où certains axiomes---possiblement tous---sont remplacés par des règles de réécriture. Le but de cette dissertation est de donner un encodage de propriétés temporelles exprimées en CTL en des formules du premier ordre, en exprimant l'équivalence logique entre les opérateurs temporels avec des règles de réécriture. De cette manière, les algorithmes de recherche de preuve conçus pour la Déduction Modulo, tels que la Résolution Modulo ou les Tableaux Modulo, peuvent être utilisés pour vérifier des propriétés temporelles de systèmes de transition finis. Afin d'accomplir le but de résoudre des problèmes de model checking avec un prouveur automatique quelconque, trois travaux sont inclus dans cette dissertation. Premièrement, nous abordons le problème de parcours de graphes en model checking avec des prouveurs automatiques. Nous proposons une façon d'encoder un graphe en tant que formule de manière à ce que le parcours du graphe correspond aux étapes de résolution. Nous présentons ensuite comment formuler les problèmes de model checking comme des formules du premier ordre en Déduction Modulo. La correction et la complétude de notre méthode montre que résoudre des problèmes de model checking CTL avec des prouveurs automatiques est faisable. Enfin, en nous appuyant sur la base théorique du deuxième travail, nous proposons une méthode de model checking symbolique. Cette méthode est implantée dans iProver Modulo, qui est un prouveur automatique du premier ordre qui utilise la Résolution Modulo Polarisée<br>Model checking is a technique for automatically verifying correctness properties of finite systems. Normally, model checking tools enjoy two remarkable features: they are fully automatic and a counterexample will be produced if the system fails to satisfy the property. . Deduction Modulo is a reformulation of Predicate Logic where some axioms- - - possibly ail---are replaced by rewrite rules. The focus of this dissertation is to give an encoding of temporal properties expressed in CTL as first -order formulas, by translating the logical equivalence between temporal operators into rewrite rules. This way, proof -search algorithms designed for Deduction Modulo, such as Resolution Modulo or Tableaux Modulo, can be used to verify temporal properties of finite transition systems. To achieve the aim of solving model checking problems with an off-the-shelf automated theorem proyer, three works are included in this dissertation. First, we address the graph traversai problems in model checking with automated theorem provers. As a preparation work, we propose a way of encoding a graph as a formula such that the traversal of the graph corresponds to resolution steps. Then we present the way of translating model checking problems as proving first-order formulas in Deduction Modulo. The soundness and completeness of our method shows that solving CTL model checking problems with automated theorem provers is feasible. At last, based on the theoretical basis in the second work, we propose a symbolic model checking method. This method is implemented in iProver Modulo, which is a first-order theorem proyer uses Polarized Resolution Modulo

Developing logic in machines has always been an area of concern for scientists. Automated Theorem Proving is a field that has implemented the concept of logical consequence to a certain level. However, if the number of available axioms is very large then the probability of getting a proof for a conjecture in a reasonable time limit can be very small. This is where the ability to learn from previously proved theorems comes into play. If we see in our own lives, whenever a new situation S(NEW) is encountered we try to recollect all old scenarios S(OLD) in our neural system similar to the new one. Based on them we then try to find a solution for S(NEW) with the help of all related facts F(OLD) to S(OLD). Similar is the concept in this research. The thesis deals with developing a solution and finally implementing it in a tool that tries to prove a failed conjecture (a problem that the ATP system failed to prove) by extracting a sufficient set of axioms (we call it Refined Axiom Set (RAS)) from a large pool of available axioms. The process is carried out by measuring the similarity of a failed conjecture with solved theorems (already proved) of the same domain. We call it "process1", which is based on syntactic selection of axioms. After process1, RAS may still have irrelevant axioms, which motivated us to apply semantic selection approach on RAS so as to refine it to a much finer level. We call this approach as "process2". We then try to prove failed conjecture either from the output of process1 or process2, depending upon whichever approach is selected by the user. As for our testing result domain, we picked all FOF problems from the TPTP problem domain called SWC, which consisted of 24 broken conjectures (problems for which the ATP system is able to show that proof exists but not able to find it because of limited resources), 124 failed conjectures and 274 solved theorems. The results are produced by keeping in account both the broken and failed problems. The percentage of broken conjectures being solved with respect to the failed conjectures is obviously higher and the tool has shown a success of 100 % on the broken set and 19.5 % on the failed ones.

Computer programs to find formal proofs of theorems were originally designed as tools for mathematicians, but modern applications are much more diverse. In particular they are used in formal methods to verify software and hardware designs to prevent errors being introduced into systems. Despite this, the high level of human expertise required in their use means that theorem proving tools are not widely used by non-specialists. The work described in this dissertation addresses one aspect of this problem, that of heuristic selection. In theory theorem provers should be automatic; in practice the heuristics used in the proof search are not universally optimal for all problems so human expertise is required to determie heuristic choice and to set parameter values. Modern machine learning has been applied to the automation of heuristic selection in a first order logic theorem prover. One objective was to find if there are any features of a proof problem that are both easy to measure and provide useful information for determining heuristic choice. Another was to determine and demonstrate a practical approach to making theorem provers truly automatic. In the experimental work, heuristic selection based on features of the conjecture to be proved and the associated axioms is shown to do better than any single heuristic. Additionally a comparison has been made between static features, measured prior to the proof search process, and dynamic features that measure changes arising in the early stages of proof search. Further work was done on determining which features are important, demonstrating that good results are obtained with only a few features required.

This dissertation is concerned with techniques for formally checking properties of systems that are described by operational semantics. We describe innovations and tools for tackling this problem, and a large case study in the application of these tools. The innovations centre on the notion of "declarative theorem proving", and in particular techniques for declarative proof description. We define what we mean by this, assess its costs and benefits, and describe the impact of this approach with respect to four fundamental areas of theorem prover design: specification, proof description, automated reasoning and interaction. We have implemented our techniques as the DECLARE system, which we use to demonstrate how our principles translate into practice. With regard to specification we briefly describe the range of specification devices employed, and present a technique for validating operational specifications against their informal requirements. The proof language is based on just three major devices: decomposition, justification by automation and second order schema application, and we describe these in detail. We also specify the requirements for an automated reasoning engine in the context of declarative proof and operational semantics. We describe the engine we have implemented and assess how it does and does not meet these requirements. The case study is a formally checked proof of the type soundness of a subset of the Java language, and is an interesting result in its own right. We define an operational semantics for this subset, based on Drossopoulou and Eisenbach's work in this field, and then outline the structure of our type soundness proot which is based on a notion of conformance. Some errors in the Java Language Specification and Drossopoulou and Eisenbach's work were discovered during this process, and these are described. Finally, we argue why declarative techniques substantially improved the quality of the results achieved, particularly with respect to maintainability and readability.