IJCAR on Friday, August 18th

Session 3: System Description 1 (09:00‑10:00)
Chair: Mark Stickel
Location: Metropolitan B

09:00‑09:15	Jürgen Zimmer (Universität des Saarlandes) Serge Autexier (DFKI) The MathServe Framework for Semantic Web Reasoning Services In recent years, formal verification of hardware and software components has increasingly attracted interest both from academia and industry. The widespread use of automated reasoning techniques requires tools that are easy to use and support standardised protocols and data exchange formats. At CADE'02 we presented the MathWeb Software Bus, our first step towards re-usable reasoning services. The MathWeb Software Bus had several drawbacks which limited its usability. For example, it had no service brokering capabilities and the user had to know exactly which reasoning system to use and how to access it. In this system description we present the MathServe system which overcomes the limitations of the MathWeb Software Bus. MathServe offers reasoning systems as Semantic Web Services described in OWL-S. A service brokering mechanism can automatically find suitable services (and service compositions) for a given reasoning problem. MathServe services and the service broker are accessed by means of standard Web Service languages and protocols.
09:15‑09:30	Predrag Janicic Pedro Quaresma (Department of Mathematics, School of Science and Technology, University of Coimbra) System Description: GCLCprover + GeoThms We present a system consisting of dynamic geometry tool and an automated theorem prover. We show how a tight integration of these modules can be achieved, and how, together with a database of geometry theorems, they provide a framework for exploring geometry problems on different levels.
09:30‑09:45	Joe Hendrix (University of Illinois at Urbana-Champaign) Jose Meseguer (University of Illinois at Urbana-Champaign) Hitoshi Ohsaki (National Institute of Advanced Industrial Science and Technology) A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms We present a tool for checking the sufficient completeness of linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.
09:45‑10:00	Allen Van Gelder (University of California, Santa Cruz) Geoff Sutcliffe (University of Miami) Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation A system is described to extend the first-order language of TPTP3 (Thousands of Problems for Theorem Provers, Version 3) to higher-order logic, primarily based on lambda-calculus expressions. The purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. The design goals were to maintain compatibility with the existing first-order TPTP3 library, to have a specification document that is understandable to researchers, to have a language that is Prolog-readable (as is the existing TPTP3 language), to have a language that is recognizable by a LALR-1 parser, such as those generated by yacc and bison, and to support the higher-order constructs in a human-readable format, using traditional conventions for lambda-calculus and typing operators. An important tool for this system is a set of Unix/Linux scripts that, with some qualifications, automatically translate the specification document into a lex scanner and yacc parser. The parser can also be built using flex and bison. The tool generates parsers that can be executed to verify compatibility with the existing TPTP3 library of problems and to parse example higher-order problems. This tool proved to be valuable for identifying and correcting several glitches (ambiguities) in the prior TPTP3 specification document. It also enabled language proposals to be rapidly debugged, leading to an extension to TPTP3 that supports higher-order constructs while remaining compatible with the existing first-order constructs. A stable proposal for extending TPTP3 to include higher-order logic is presented.

Break (10:00‑10:30)

Session 4: Higher-Order Logic (10:30‑12:30)
Chair: Michael Kohlhase
Location: Metropolitan B

10:30‑11:00	Robert Constable (Cornell University) Wojciech Moczydlowski (Cornell University) Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics Church's Higher Order Logic is a basis for proof assistants --- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard set theory, ZFC, into a constructive core, IZF, and axioms of excluded middle and choice. Then we provide the standard set-theoretic semantics in such a way that the constructive core of HOL is mapped into IZF. We use the disjunction, numerical existence and term existence properties of IZF to provide a program extraction capability from proofs in the constructive core. We can implement the disjunction and numerical existence properties in two different ways: one modifying Rathjen's realizability for CZF and the other using a new direct weak normalization result for intensional IZF by Moczydlowski. The latter can also be used for the term existence property.
11:00‑11:30	John Harrison (Intel Corporation) Towards self-verification of HOL Light The HOL Light prover is based on a logical kernel consisting of about 400 lines of mostly functional OCaml, whose complete formal verification seems to be quite feasible. We would like to formally verify (i) that the abstract logic HOL is supposed to implement is indeed correct, and (ii) that the OCaml code does correctly implement this logic. We have performed a verification of the basic HOL Light core, without definitional mechanisms, and this verification is entirely conducted within HOL Light itself. We will duly explain why the obvious logical and pragmatic difficulties do not vitiate this approach, even though it looks impossible or useless at first sight. Extension to include definitional mechanisms seems straightforward enough, but the results so far allay most of our practical worries.
11:30‑12:00	Sean McLaughlin (Carnegie Mellon University) An Interpretation of Isabelle/HOL in HOL Light We define an interpretation of the Isabelle/HOL logic in the logic of the HOL Light theorem prover. The interpretation takes the form of a set of elaboration rules, where features of the logic which cannot be represented directly are represented as functors in Ocaml, HOL Light's metalanguage. We demonstrate the effectiveness of the interpretation by translating a large body of the Isabelle standard library into HOL Light. We also provide a simple specification language for extending the translation to new theories. After minimal user specification, the translation is automatic.
12:00‑12:30	Chad E. Brown (Universitaet des Saarlandes) Combining Type Theory and Untyped Set Theory We describe a second-order logical framework with proof irrelevance. Within this framework, we give a representation of a form of Mac Lane set theory and discuss automated support for constructing proofs within this set theory. One of the novel aspects of the representation is that one is allowed to any class (in the set theory) as a type (in the logical framework). Such class types allow a natural way of representing partial functions (e.g., the first and second operators on the class of Kuratowski ordered pairs). We also discuss how automated search can be used to construct proofs. In particular, the first-order prover Vampire can be called to solve a challenge problem (the injective Cantor Theorem) which is notoriously difficult for higher-order automated provers.

Lunch break (12:30‑14:00)

Session 5: Proof Theory (14:00‑16:00)
Chair: Matthias Baaz
Location: Metropolitan B

14:00‑14:30	Christoph Benzmüller (Saarland University, Germany) Chad E. Brown (Universitaet des Saarlandes) Michael Kohlhase (International University Bremen) Cut-Simulation in Impredicative Logics We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic --- in our case a sequent calculus for classical type theory --- is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and description. For improving the automation of proof search in impredicative logics this calls for the development of calculi where these principles are built-in instead of being treated axiomatically.
14:30‑15:00	Viorica Sofronie-Stokkermans (Max Planck Institute for Computer Science) Interpolation in local theory extensions Many problems in mathematics and computer science (e.g. in verification, or when reasoning in and about distributed databases) can be reduced to proving the satisfiability of conjunctions of (ground) literals modulo a background theory. This theory can, for instance, be the extension of a base theory with additional functions or a combination of theories. It is therefore very important to find efficient methods for checking the unsatisfiability of ground formulae in such complex theories. However, it is often equally important to find local causes for inconsistency. Such information is usually provided by interpolants. In this paper we study interpolation in local extensions of a base theory ${\cal T}_0$. In such extensions efficient hierarchical reasoning - in which a prover for the base theory is used as a black box - is possible. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in ${\cal T}_0$ as `black-boxes' in order to generate interpolants in the extension. We provide several examples of such theories, and discuss their applications in verification or knowledge representation.
15:00‑15:30	Anna Zamansky (Tel Aviv university) Arnon Avron (Tel Aviv university) Canonical Gentzen-type calculi with (n,k)-ary quantifiers Propositional canonical Gentzen-type systems, introduced by Avron&Lev, are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a connective is introduced and no other connective is mentioned. Avron&Lev provide a constructive coherence criterion for the non-triviality of such systems and show that a system of this kind admits cut-elimination iff it is coherent. The semantics of such systems is provided by two-valued non-deterministic matrices (2Nmatrices). Zamansky&Avron extend these results to systems with unary quantifiers of a very restricted form. In this paper we substantially extend the scope of the characterization of canonical systems to (n,k)-ary quantifiers, which bind k distinct variables and connect n formulas. We show that the coherence criterion is constructive for such systems, and that for the case of k=0 or k=1: (i) a canonical system is coherent iff it has a strongly characteristic 2Nmatrix, and (ii) if a canonical system is coherent, then it admits cut-elimination.
15:30‑16:00	Bernhard Beckert (University of Koblenz) Andre Platzer (University of Oldenburg) Dynamic Logic with Non-rigid Functions In this paper, we introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution). And we present a (relatively) complete sequent calculus for this logic. In conjunction with dynamically typed object enumerators, non-rigid functions allow to embed notions of object-orientation in dynamic logic, thereby forming a basis for verification of object-oriented programs. A semantical generalisation of substitutions, called state update, which we add to the logic, constitutes the central technical device for dealing with object aliasing during function modification. With these few extensions, our dynamic logic captures the essence of the verification system \KeY and, hence, constitutes a foundation for object-oriented verification with the principles of reasoning that underly the successful \KeY case studies.

Break (16:00‑16:30)

Invited Talk (16:30‑17:30)
Chair: Ulrich Furbach
Location: Metropolitan B

16:30‑17:30

Adnan Darwiche (University of California, Los Angeles) Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation [ppt] I will discuss in this talk two influential areas of automated reasoning, satisfiability and knowledge compilation. Historically, these two areas have been developing independently, but have come to an intersection point recently that is interesting both theoretically and practically. In particular, I will show that the intersection point rests on recent extensions of satisfiability solvers to perform exhaustive searches for the purpose of model counting and enumeration, aided by sophisticated techniques such as component analysis and formula caching. More precisely, I will show that the traces of these exhaustive search algorithms can be interpreted as sentences and that each search algorithm corresponds to a (tractable) language generated by all its possible executions. I will provide multiple matches between key search algorithms and well known tractable languages and discuss two implications of this matching: (1) harnessing advances in satisfiability to compile knowledge bases, leading to some new algorithms for knowledge compilation, and (2) invoking known results on tractable languages to identify previously unknown powers and limitations of search algorithms. The talk will provide ample empirical results and applications from various areas, including planning, diagnosis and probabilistic reasoning.

CAV-IJCAR Joint Cruise/Banquet (19:00‑22:30)
Location: depart Spirit of Seattle from Pier 55

19:00‑19:30	CAV-IJCAR Joint Cruise/Banquet Boarding from Pier 55 (walking distance from hotel)
19:30‑22:30	CAV-IJCAR Joint Cruise/Banquet