IJCAR on Sunday, August 20th

Invited Talk (09:00‑10:00)
Chair: Natarajan Shankar
Location: Grand Ballroom B

09:00‑10:00

Dale Miller (INRIA and LIX/Ecole Polytechnique) Representing and Reasoning With Operational Semantics [pdf] The operational semantics of programming and specification languages is often presented via inference rules and these can generally be mapped into logic programming-like clauses. Such encodings of operational semantics can be surprisingly declarative if one uses logics that directly account for term-level bindings and for resources, such as are found in linear logic. Traditional theorem proving techniques, such as unification and backtracking search, can then be applied to animate operational semantic specifications. Of course, one wishes to go further than animation: using logic to encode computation should facilitate formal reasoning directly with semantic specifications. We outline an approach to reasoning about operational semantics where semantic specifications are encoded as theories in an object-logic and where properties of the semantic specification are inferred in a meta-logic. We motivate the design goals of a meta-logic that has been built for that purpose.

Break (10:00‑10:30)

Session 11: Decision Procedures (10:30‑12:30)
Chair: Maria Paola Bonacina
Location: Grand Ballroom B

10:30‑11:00	Maria Paola Bonacina Silvio Ghilardi (Dipartimento di Informatica, Università degli Studi di Milano (Italia)) Enrica Nicolini Silvio Ranise (LORIA-INRIA & U. Milano) Daniele Zucchelli Decidability and Undecidability Results for Nelson-Oppen and Rewrite-based Decision Procedures In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in finite and infinite models, respectively. We exhibit a theory $T_1$ such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in $T_1\cup T_2$ is undecidable, whenever $T_2$ has only infinite models, even if signatures are disjoint and satisfiability in $T_2$ is decidable. In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either finite or infinite models, is decidable. We show that this result covers decision procedures based on rewriting, generalizing recent work on combination of theories in the rewrite-based approach to satisfiability.
11:00‑11:30	Amine Chaieb (TU Muenchen) Verifying mixed real-integer quantifier elimination We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination procedures: for Presburger arithmitics and for linear real arithmetics.
11:30‑12:00	Stephane Demri (LSV, ENS de Cachan) Denis Lugiez (LIF, Marseille) Presburger Modal Logic is Only PSPACE-complete We introduce a Presburger modal logic PML with regularity constraints and full Presburger constraints on the number of children that generalize graded modalities, also known as number restrictions in description logics. We show that PML satisfiability is only PSPACE-complete by designing a Ladner-like algorithm. This extends a well-known and non-trivial PSPACE upper bound for graded modal logic. Furthermore, we provide a detailed comparison with logics that contain Presburger constraints and that are dedicated to query XML documents. As an application, we show that satisfiability for Sheaves Logic SL is PSPACE-complete, improving significantly its best known upper bound.
12:00‑12:30	Florent Jacquemard (INRIA & LSV) Michael Rusinowitch (LORIA) Laurent Vigneron (LORIA - University Nancy 2) Tree automata with equality constraints modulo equational theories This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in program verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.

Session 12: CASC Results (10:30‑11:30)
Chair: Geoff Sutcliffe
Location: Willow A

Lunch break (12:30‑14:00)

Session 13: Description Logic (14:00‑15:30)
Chair: Ian Horrocks
Location: Grand Ballroom B

14:00‑14:30	Daniel Dougherty (WPI) Kathi Fisler (WPI) Shriram Krishnamurthi (Brown University) Specifying and Reasoning about Dynamic Access-Control Policies Access-control policies have grown from simple matrices to non-trivial specifications written in sophisticated languages. The increasing complexity of these policies demands correspondingly strong automated reasoning techniques for understanding and debugging them. The need for these techniques is even more pressing given the rich and dynamic nature of the environments in which these policies evaluate. We define a framework to represent the behavior of access-control policies in a dynamic environment. We then several interesting, decidable analyses using-order temporal logic. Our work illustrates the subtle interplay between logical and state-based methods, particularly in the presence of three-valued policies. We also define a notion of policy equivalence that is especially useful for modular reasoning.
14:30‑15:00	David Toman (University of Waterloo) Grant Weddell (University of Waterloo) On Keys and Functional Dependencies as First-class Citizens in Description Logics We investigate whether identification constraints can be granted full status as a concept constructor in a Boolean-complete description logic. In particular, we show that surprisingly simple forms of such constraints lead to undecidability of the associated logical implication problem if they are allowed within the scope of a negation or on the left-hand-side of inclusion dependencies. We then show that allowing a very general form of identification constraints to occur in the scope of monotone concept constructors on the right-hand-side of inclusion dependencies will still lead to decidable implication problems. Finally, we consider the relationship between certain classes of identification constraints and nominals.
15:00‑15:30	Yevgeny Kazakov (University of Manchester) Boris Motik (University of Manchester) A Resolution-Based Decision Procedure for SHOIQ We present a resolution-based decision procedure for the description logic SHOIQ---the logic underlying the Semantic Web ontology language OWL-DL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Applying existing techniques for saturation-based decision procedures to SHOIQ is not straightforward due to nominals, number restrictions, and inverse roles---a combination known to cause termination problems. We overcome this difficulty by using the basic superposition calculus, extended with custom simplification rules.

Break (15:30‑16:00)

Session 14: Rewriting (16:00‑18:00)
Chair: Aart Middeldorp
Location: Grand Ballroom B

16:00‑16:30	Joerg Endrullis (Vrije Universiteit Amsterdam) Johannes Waldmann (HTWK Leipzig, FB IMN) Hans Zantema (Technische Universiteit Eindhoven) Matrix Interpretations for Proving Termination of Term Rewriting We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular non-total well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows to prove termination and relative termination. A modification of the latter in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver. Our implementation performs well on the Termination Problem Data Base: better than 5 out of 6 tools that participated in the 2005 termination competition in the category of term rewriting.
16:30‑17:00	Alexander Krauss (Technische Universität München) Partial Recursive Functions in Higher-Order Logic Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for them. Our method expresses termination in a uniform manner and includes a very general form of pattern matching, where patterns can be arbitrary expressions. Termination proofs can be deferred, limited to subsets of arguments and are interchangeable with other proofs about the function. We show that this approach can also facilitate termination arguments for total functions, in particular for nested recursions. We implemented our tool as a definitional specification mechanism for Isabelle/HOL.
17:00‑17:30	Benjamin Werner (INRIA and Ecole polytechnique) On the strength of proof-irrelevant type theories We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is particularly useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. Finally we show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is almost classical logic.
17:30‑18:00	Daria Walukiewicz-Chrząszcz (Warsaw University) Jacek Chrząszcz (Warsaw University) Consistency and Completeness of Rewriting in the Calculus of Constructions Adding rewriting to a proof assistant based on the Curry-Howard isomorphism, such as Coq, may greatly improve usability of the tool. Unfortunately adding an arbitrary set of rewrite rules may render the underlying formal system undecidable and inconsistent. While ways to ensure termination and confluence, and hence decidability of type-checking, have already been studied to some extent, logical consistency has got little attention so far. In this paper we show that consistency is a consequence of canonicity, which in turn follows from the assumption that all functions defined by rewrite rules are complete. We provide a sound and terminating, but necessarily incomplete algorithm to verify this property. The algorithm accepts all definitions that follow dependent pattern matching schemes presented by Coquand and studied by McBride in his PhD thesis. Moreover, many definitions by rewriting containing rules which depart from standard pattern matching are also accepted.