| Christopher Lynch. Unsound Theorem Proving |
| Abstract: We discuss the benefits of complete unsound inference procedures for efficient methods of disproof. We give a framework for converting a sound and complete saturation-based inference procedure into successive unsound and complete procedures, that serve as successive approximations to the theory. The idea is to successively add new statements in such a way that the inference procedure will halt. Then the satisfiability is evaluated over a stronger theory. We illustrate this framework with Knuth-Bendix Completion, and show that in some theories these successive approximations become weaker and weaker, and sometimes become a decision problem. Then we illustrate the framework with a new method for the (nonground) word problem, based on Congruence Closure. We show a class where this becomes a decision procedure. Also, we show that this new inference system is interesting in its own right. Given a particular goal, in many cases we can halt the procedure at some point and say that all the equations for solving the goal have been generated already. This is generally not possible in Knuth-Bendix Completion. |
| Simon Colton and Alison Pease. The TM System for Repairing Non-Theorems |
| Abstract: We describe a flexible approach to automated reasoning, where non-theorems can be automatically altered to produce proved results which are related to the original. This is achieved through an interaction of the HR machine learning system, the Otter theorem prover and the Mace model generator, and uses methods inspired by Lakatos's philosophy of mathematics. We demonstrate the effectiveness of this approach by modifying non-theorems taken from the TPTP library of first order theorems. |
| Tjark Weber. Bounded Model Generation for Isabelle/HOL |
| Abstract: A translation from higher-order logic (on top of the simply typed $\lambda$-calculus) to propositional logic is presented, such that the resulting propositional formula is satisfiable iff the HOL formula has a model of a given finite size. A SAT solver can then be used to search for a satisfying assigment, and such an assignment can be transformed back into a model for the HOL formula. The algorithm has been implemented in Isabelle/HOL, where it is used to automatically generate countermodels for non-theorems. |
| Jian Zhang. Reducing Symmetries to Generate Easier SAT Instances |
| Abstract: Finding countermodels is an effective way of disproving false conjectures. In first-order predicate logic, model finding is an undecidable problem. But if a finite model exists, it can be found by exhaustive search. The finite model generation problem in the first-order logic can also be translated to the satisfiability problem in the propositional logic. But a direct translation may not be very efficient. This paper discusses how to take the symmetries into account so as to make the resulting problem easier, and reports some experimental results. |
| Alan Bundy. (Invited Talk) Finding and Using Counter-Examples |
| Abstract:
Disproving conjectures, either by finding counterexamples or by refutation, is a neglected part of automated reasoning compared to proving theorems. Despite this neglect, it is an extremely important part of reasoning. For instance, in formal methods, implementations are notoriously error prone, and seldom meet their specifications. Moreover, industrial users of formal verification tools are much more likely to be impressed that a previously unsuspected, but important, bug was discovered than they are with a proof that a system is bug-free, especially when bugs are subsequently revealed during unanticipated uses of the system or when it is coupled to other components. It is time to reverse this neglect and give disproof the attention it deserves. In this talk I will survey recent work in my research group on the detection and use of counter-examples to conjectures. This will include the automatic detection of counter-examples by the analysis of failed proofs, the use of refutation complete provers and testing against standard models. We will describe how these counterexamples can be used, for instance, to automatically generate attacks on security protocols, including previously unknown attacks on group protocols. Counterexamples can also be used to prevent theorem *proving* systems from wasting time proving false subgoals. Finally, we will discuss how counterexamples can be used automatically correct faulty conjectures. The work reported is joint with Raul Monroy, Louise Dennis, Simon Colton, Alison Pease and Graham Steel. |
| Louise Abigail Dennis. The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs |
| Abstract: This paper reports the use of proof planning to diagnose errors in program code. In particular it looks at the errors that arise in the base cases of recursive programs produced by undergraduates. It describes two classes of error that arise in this situation. The use of test cases would catch these errors but would fail to distinguish between them. The system adapts proof critics, commonly used to patch faulty proofs, to diagnose such errors and distinguish between the two classes. It has been implemented in lambda-clam, a proof planning system, and applied successfully to a small set of examples. |
| Didier Galmiche and Daniel Mery. Resource Graphs and Countermodels in Resource Logics |
| Abstract: In this abstract, we aim to emphasize the role of a semantic structure called dependency (or resource) graph in order to study the provability in some resource sensitive logics, like the Bunched Implications Logic (BI) or the Non-commutative Logic (NL) and mainly to provide countermodels. Such a semantic structure is appropriate to capture the particular interactions between different kinds of connectives (additives and multiplicatives in BI and commutatives and non commutatives in NL) during both proof and countermodel search. In order to illustrate the main ideas and results based on labels, constraints and resource graphs, we consider the BI logic with a based-on tableaux approach. We also describe tools implemented for countermodel generation (BILL) or verification (checkBI) in this resource logic. |
| Dominique Larchey-Wendling. Gödel-Dummett counter-models through matrix computation |
| Abstract: We present a new method for deciding Gödel-Dummett logic. Starting from a formula, it proceeds in three steps. First build a conditional graph based on the decomposition tree of the formula. Then try to remove some cycles in this graph by instantiating these boolean conditions. In case this is possible, extract a counter-model from such an instance graph. Otherwise the initial formula is provable. We emphasize on cycle removal through matrix computation, boolean constraint solving and counter-model extraction. |