| Cesare Tinelli Trends and Challenges in Satisfiability Modulo Theories |
| Abstract: Satisfiability Modulo Theories (SMT) is concerned with the problem of determining the satisfiability of first-order formulas with respect to a given logical theory T. A distinguishing feature of SMT is the use of inference methods tailored to the particular theory T. By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, ground formulas), such methods can be implemented into solvers that are more efficient in practice than general-purpose theorem provers. SMT techniques have been traditionally developed to support deductive software verification, but they have also applications in model checking, certifying compilers, automated test generation, and other formal methods. This talk gives an overview of SMT and its applications, and highlights some long-standing challenges for a wider applications of SMT techniques within formal methods, as well as some fresh challenges introduced by new potential uses. A major challenge is providing adequate model generation features for disproving verification conditions. |
| Alan Bundy Where's My Stuff? An Ontology Repair Plan |
| Abstract: Appropriate representation is the key to successful reasoning. Hence, if intelligent agents are to cope with changing goals in a changing environment, they must be able to adapt their representations, i.e., to detect that a current representation is inadequate, to diagnose its shortcomings and to repair it. In this paper we address the most basic kind of representational shortcoming: inconsistency. We focus on how certain kinds of inconsistency can be repaired using a repair plan that we entitle Where's My Stuff?. We apply this repair plan manually to four examples from the domain of Physics. In each case an inconsistent ontology is repaired into a consistent one. This extends the interest of the Disproving workshop beyond the "reparation of non-theorems" to the reparation of inconsistent ontologies. The Physics domain has the advantage that many faulty ontologies have been recorded by historians of science, together with the evidence that identified their faults and the ontological repairs that were proposed to mend them. |
| Arjeh M. Cohen, Jan Willem Knopper, and Scott H. Murray. Automatic Proof of Graph Nonisomorphism |
| Abstract: We describe automated methods for constructing nonisomorphism proofs for pairs of graphs. The proofs can be human-readable or machine-readable. We have developed a proof generator for graph nonisomorphism, which allows users to input graphs and construct a proof of (non)isomorphism. |
| Koen Claessen. A Paradigm Shift in ATP: Towards Model-based Reasoning Systems |
| Abstract: Traditionally and historically, ATP systems have been used in a rather specialized way. The problems they solved were relatively small, and almost always constructed by hand, very often by an expert on ATP systems (if not the actual creator of the ATP system at hand). In this way, if a problem could not be proved by a system, the behavior of the system could somehow be understood by the constructor of the problem, and the problem was tweaked, for example by changing an axiom, or adding new assumptions. When a problem was difficult, this usually was caused by the proof of the problem being complex. A paradigm shift in the use of ATP systems has happened over the last number of years. Problems are not being created only by ATP experts anymore. Novel areas for applications of ATP systems for first-order logic keep popping up; areas whose contents have very little to do with ATP systems, and whose active members are not experts on ATP. People are automatically generating problems for ATP systems from other formalisms. The problem sizes are steadily increasing. Axiomatizations are not carefully crafted anymore. For many application areas, problems are not difficult anymore simply because their proofs are complex; new problems are often difficult because the proofs, which are relatively small, are hard to find - there is often a lot of "junk" irrelevant to the proof, but clogging up the proof search. In this talk, I would like to argue for the necessity of a corresponding paradigm shift in ATP system design. The key feature that is lacking in almost all of today's most powerful ATP systems is feedback in the case of a failed proof. Most ATP systems simply never terminate when presented with a problem that they cannot solve (in some lucky cases termination does occur when a saturation or a finite model has been found). SAT-solvers I would like to draw a parallel with the development in the area of SAT-solvers. Today, SAT-solvers are (literally) routinely used as black box procedures in many different application areas. There are two key features that make this possible. The first feature is feedback; when a SAT-solver terminates, it actually produces more than just a "yes" or a "no" answer. When a problem is deemed satisfiable, an actual model is produced as the result. For most SAT-based algorithms it is vital that this model is produced. Quite quickly after the developments in the SAT community that made SAT-solvers practical, users of SAT-solvers realized that they also wanted feedback when a problem was deemed unsatisfiable. In this case, the SAT-solver can produce a proof of unsatisfiability. The second feature is incrementality. After feedback has been examined by the caller of the SAT-solver, small changes can be made to the problem (usually automatically), and the SAT-solver can be run again, reusing as much information from the previous run as possible. Some of the most industrially successful applications of SAT-solvers (for example interpolant-based model checking) critically depend on getting useful feedback from the SAT-solver in both the "yes" and the "no" case, and the use of incrementality. First-order Logic In first-order logic, things do not look as bright. Although there are a number of areas where ATP systems have successfully been used as black boxes, very little feedback is provided from today's ATP systems. When a proof is found, most systems are able to produce this. When a proof cannot be found, the result of the ATP system does not contain any kind of reason why not. If we want our ATP systems to be used by non-experts, we need to provide feedback for failed proofs that can be understood by non-experts. Even more important, if we want our ATP systems to be used as a black box component inside a larger system, it is vital that the ATP system provides feedback about why it could not find a proof to its caller! Incremental use of a system is empowered by an order of magnitude if useful feedback is provided between calls. The kind of feedback I propose to use is that of a candidate counter model. One reason why we cannot simply copy what happens in the world of SAT-solvers is that first-order logic is semi-decidable, which means that we cannot always (or rather: we can very seldomly) produce an actual counter model of the problem if there does not exist a proof. What we can do however, is to produce a candidate counter model. A candidate counter model can be seen as an approximation of a real counter model; the longer time the ATP system runs, the closer to a real counter model the candidate counter model becomes. In the talk, I will describe what such a candidate counter model is, some theory behind it, how candidate counter models can be found, and how they can be used. It turns out that it is very natural for an ATP system that produces candidate counter models to be instance based. We present some experimental evidence that instance based (and thus model-based) methods actually are a very good fit with the above mentioned paradigm shift in ATP usage. I will also discuss the impact that a model-based view has on the internal design of an ATP system; for example, it becomes very important to deal with typed problems, and even basic algorithms such as clausification should be revisited! |
| Jan Otop Solution to some right alternative ring problems |
| Abstract: In this paper we show a computer construction of a counterexample to the TPTP problems RNG030 and RNG032. These problems have been open up to now. The used method share some ideas with the Z-module method, but it is more semantic oriented. We deal also with ensuring program correctness. It is harder than in case of proving theorem, because there is no succinct "proof". |
| Didier Galmiche, Dominique Larchey-Wendling and Yakoub Salhi Provability and Countermodels in Gödel-Dummett Logics |
| Abstract: Hypersequent calculi, that are a generalization of sequent calculi, have been studied for Goedel-Dummett logics LC and LCn. In this paper we propose a new characterization of validity in these logics from the construction of particular bi-colored graphs associated to hypersequents and the search of specific chains in such graphs. It leads to other contributions that are a new hypersequent calculus and a related tableau system for LCn. We mainly study the class of so-called basic hypersequents and then we generalize our approach to hypersequents. |
| Hans de Nivelle Redundancy for Geometric Resolution |
| Abstract: We study redundancy for geometric resolution. It is known from experiments with superposition that a large part of its success can be attributed to the associated simplification rules. Based on this observation, it is a natural question to ask whether geometric resolution also admits simplification rules, and what form they can have. In this paper, we try to an answer this question. We first describe 3 simplification rules that have been implemented in geo. Two of these simplification rules were successful. One was not. It can be shown that all three of these simplification rules are complete. From this we conclude that, unlike for superposition, a semantic completeness proof is not useful for establishing the effectiveness of a simplification rule. In the rest of hte paper, we develope a proof theoretic framework, in which the effect of a simplification can be modelled by proof transformations. This framework is able to explain the distinct behaviour of the three refinements, but it is too early to decide (mainly because of too little examples) whether it can provide a complete classification. |