IJCAR on Saturday, July 17th

09:00‑10:00 Invited Talk
Location: AT LT5
09:00 Johan van Benthem (Stanford University and University of Amsterdam)
Logic between Expressivity and Complexity

Automated deduction is not just application or implementation of logical systems. The field of computational logic also poses deep challenges to our understanding of logic itself. I will discuss some key issues.

10:30‑12:30 Verification
Location: AT LT5
10:30 Ali Ayad and Claude Marché
Multi-Prover Verification of Floating-Point Programs

In the context of deductive program verification, supporting floating-point computations in a sound way is tricky. We propose an expressive language to formally specify behavioral properties of such programs. We give a first-order axiomatization of floating-point operations which allows to reduce verification to checking the validity of logic formulas, in a suitable form for a large class of provers including SMT solvers and interactive proof assistants. Experiments using the Frama-C platform for static analysis of C code are presented.

11:00 Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport and Stephan Merz
Verifying Safety Properties With the TLA+ Proof System

The TLA+ proof system is a platform for the development and mechanical verification of correctness proofs of TLA+ system specifications. The proof language is declarative, supports hierarchical and non-linear proof construction and verification, and is designed to be independent of any particular verification tool or strategy. A Proof Manager tool interprets TLA+ proofs and invokes a collection of certifying theorem provers, proof assistants, SMT solvers and decision procedures to verify the proof. The initial public version of the proof system described here supports reasoning about most of the non-temporal parts of TLA+, and has just enough support for temporal reasoning to verify standard safety properties.

11:15 Ruzica Piskac and Viktor Kuncak
MUNCH - Automated Reasoner for Sets and Multisets

This system description provides an overview of a reasoner for sets and multisets. The MULTI-SETS reasoner takes a formula in a logic that support expressions about sets, multisets, integers, and uninterpreted functions computing set images. Constraints over collections and integers are connected using the cardinality operator. This logic is a fragment of a logic for various interactive theorem provers. We provide the first fully automated reasoner for this logic. The reasoner reduces input formulas to equisatisfiable linear integer arithmetic formulas. The MULTI-SETS reasoner is implemented in Scala and integer linear arithmetic constraints are solved by invoking the SMT solver z3.

11:30 Elena Sherman, Brady J. Garvin and Matthew B. Dwyer
A Slice-based Decision Procedure for Type-based Partial Orders

Automated software verification and path-sensitive program analysis require the ability to distinguish executable program paths from those that are infeasible. To achieve this, program paths are encoded symbolically as a conjunction of constraints and submitted to an SMT solver; satisfiable path constraints are then analyzed further.

In this paper, we study type-related constraints that arise in path-sensitive analysis of object-oriented programs with forms of multiple inheritance. The dynamic type of a value is critical in determining program branching related to dynamic dispatch, type casting, and explicit type tests. We develop a custom decision procedure for queries in a theory of type-based partial orders and show that the procedure is sound and complete, has low complexity, and is amenable to integration into an SMT framework. We present an empirical evaluation that demonstrates the speed and robustness of our procedure relative to Z3.

12:00 Viorica Sofronie-Stokkermans
Hierarchical reasoning for the verification of parametric systems

We study certain classes of verification problems for parametric reactive and hybrid systems, and identify the types of logical theories which can be used for modeling such systems and the reasoning tasks which need to be solved in this context. We identify properties of the underlying theories which ensure that these classes of verification problems can be solved efficiently, give examples of theories with the desired properties, and illustrate the methods we use on several examples.

14:00‑15:00 First-Order Logic
Location: AT LT5
14:00 Krystof Hoder, Laura Kovacs and Andrei Voronkov
Symbol Elimination and Interpolation in Vampire

It has recently been shown that proofs in which some symbols are colored (e.g. local or split proofs and symbol-eliminating proofs) can be used for a number of applications, such as invariant generation and computing interpolants.

This tool paper describes how such proofs and interpolant generation are implemented in the first-order theorem prover Vampire.

14:15 Konstantin Korovin and Christoph Sticksel
iProver-Eq: An Instantiation-based Theorem Prover with Equality

iProver-Eq is an implementation of an instantiation-based calculus Inst-Gen-Eq which is complete for first-order logic with equality. iProver-Eq extends the iProver system with rewrite-based equational reasoning and maintains the distinctive features of the Inst-Gen method. In particular, first-order reasoning is combined with efficient ground satisfiability checking where the latter is delegated in a modular way to any state-of-the-art SMT solver. The first-order reasoning employs a saturation algorithm with means of redundancy elimination such as blocking and simplification inferences. We describe the equational reasoning as it is implemented in iProver-Eq, the main challenges and techniques that are essential for efficiency.

14:30 Hans de Nivelle
Classical Logic with Partial Functions

We give a natural semantics for classical logic with partial functions. The semantics makes use of multi-valued logic, so that formulas involving undefined values can have undefined truth values. An unusual aspect of our semantics is that it relies on the order of formulas. In this way, the semantics is able to capture the fact that functions and predicates must be declared before they are used.

After that, we define a sequent calculus and prove the calculus sound and complete with respect to the semantics that we introduced.

We think that our approach to partial functions is more natural than existing approaches, because in our approach, formulas involving undefined values are guaranteed to be undefined. For example, it captures realistic behavior of programs involving undefined values. The outcome of such programs should be undefined, even in cases where an outcome can be deduced in principle.

15:30‑17:00 Non-Classical Logic
Location: AT LT5
15:30 Christoph Beierle, Marc Finthammer, Gabriele Kern-Isberner and Matthias Thimm
Automated Reasoning for Relational Probabilistic Knowledge Representation

KReator is a toolbox for representing, learning, and automated reasoning with various approaches combining relational first-order logic with probabilities. We give a brief overview of the KReator system and its automated reasoning facilities.

15:45 Rajeev Goré and Florian Widmann
Optimal Tableaux for Propositional Dynamic Logic with Converse

We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound method to combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.

16:15 Mark Kaminski and Gert Smolka
Terminating Tableaux for Hybrid Logic with Eventualities

We present the first terminating tableau system for hybrid logic with eventualities. The system is designed as a basis for gracefully degrading reasoners. Eventualities are formulas of the form <>*s that hold for a state if it can reach in n>=0 steps a state satisfying the formula s. The system is prefix-free and employs a novel clausal form that abstracts away from propositional reasoning. It comes with an elegant correctness proof. We discuss some optimizations for decision procedures.

16:45 Marta Cialdea Mayer and Serenella Cerrito
Herod and Pilate: two tableau provers for basic hybrid logic

This work presents two provers for basic hybrid logic HL(@), which have been implemented with the aim of comparing two internalized tableau calculi independently proposed, respectively, by Bolander and Blackburn (2007) and Cerrito and Cialdea Mayer (2007). Such calculi bear strong similarities, but essentially differ in the treatment of nominal equalities: while the first adopts a declarative approach, the second handles equalities by means of explicit substitution and nominal deletion. Experimental results are reported, evaluating, from the practical point of view, the different treatment of nominal equalities in the two calculi, and showing that substitution with nominal deletion has meaningful practical advantages.

17:10‑18:30 Business Meetings (held at Forum building)
Location: AT LT5
17:10 CADE Business Meeting
17:50 Tableaux Business Meeting