CADE on Sunday

Detailed program
Sunday July 28th, 2002
See also the unified by-slot program

Sessions take place in auditorium 3 unless otherwise indicated.

All-day activities

Session 5: SAT

09:00-09:30  Eugene Goldberg, Cadence Design Systems, USA
Testing satisfiability of CNF formulas by computing a stable set of points
We show that a conjunctive normal form (CNF) formula F is unsatisfiable iff there is a set of points of the Boolean space that is stable with respect to F. So testing the satisfiability of a CNF formula reduces to looking for a stable set of points (SSP). We give some properties of SSPs and describe a simple algorithm for constructing an SSP for a CNF formula. Building an SSP can be viewed as a "natural" way of search space traversal. This naturalness of search space examination allows one to make use of the regularity of CNF formulas to be checked for satisfiability. We illustrate this point by showing that if a CNF F formula is symmetric with respect to a group of permutations, it is very easy to make use of this symmetry when constructing an SSP. As an example, we show that the unsatisfiability of pigeon-hole CNF formulas can be proven by examining only a set of points whose size is quadratic in the number of holes.

09:30-10:00  Thierry Boy de la Tour, IMAG Grenoble, France
A note on symmetry heuristics in SEM
We analyse two symmetry heuristics, i.e. heuristics that reduce the search space through properties of symmetry, in the finite model generator SEM. These are SEM's original LNH, and a recent extension XLNH. Our aim is to show how a simple group-theoretic framework brings much clarity in this matter, especially through group actions. Both heuristics can be seen as computationally efficient ways of applying a general symmetry pruning theorem. Moreover, simple combinatorics provide some insight into the relative performances of these heuristics. We finally expose a fundamental difficulty in making SEM symmetry efficient by symmetry pruning.

10:00-10:30  Gilles Audemard, ITC-irst, Italy
Piergiorgio Bertoli, ITC-irst, Italy
Alessandro Cimatti, ITC-irst, Italy
Artur Kornilowicz, ITC-irst, Italy
Roberto Sebastiani, ITC-irst, Italy
A SAT based approach for solving formulas over boolean and linear mathematical propositions
The availability of decision procedures for combinations of boolean and linear mathematical propositions opens the ability to solve problems arising from real-world domains such as verification of timed systems and planning with resources. In this paper we present a general and efficient approach to the problem, based on two main ingredients. The first is a DPLL-based SAT procedure, for dealing efficiently with the propositional component of the problem. The second is a tight integration, within the DPLL architecture, of a set of mathematical deciders for theories of increasing expressive power. A preliminary experimental evaluation shows the potential of the approach.

Session 6: Model generation

11:00-11:30  Wolfgang Ahrendt, Chalmers U of Techn., Sweden
Deductive search for errors in free data type specifications using model generation
The presented approach aims at identifying false conjectures about free data types. Given a specification and a conjecture, the method performs a search for a model of an according counter specification. The model search is tailor-made for the semantical setting of free data types, where the fixed domain allows to describe models just in terms of interpretations. For sake of interpretation construction, a theory specific calculus is provided. The concrete rules are `executed' by a procedure known as model generation. As most free data types have infinite domains, the ability of automatically solving the non-consequence problem is necessarily limited. That problem is addressed by limiting the instantiation of the axioms. This approximation leads to a restricted notion of model correctness, which is discussed. At the same time, it enables model completeness for free data types, unlike approaches based on limiting the domain size.

11:30-12:00  Gilles Audemard, ITC-irst, Italy
Belaid Benhamou, LSIS Marseille, France
Reasoning by symmetry and function ordering in finite model generation
Finite model search for first-order logic theories is complementary to theorem proving. Systems like Falcon, SEM and FMSET use the known LNH (Least Number Heuristic) heuristic to eliminate some trivial symmetries. Such symmetries are worthy, but their exploitation is limited to the first levels of the model search tree, since they disappear as soon as the first cells have been interpreted. The symmetry property is well-studied in propositional logic and CSPs, but only few trivial results on this are known on model generation in first-order logic. We study in this paper both an ordering strategy that selects the next terms to be interpreted and a more general notion of symmetry for finite model search in first-order logic. We give an efficient detection method for such symmetry and show its combination with the trivial one used by LNH and LNHO heuristics. This increases the efficiency of finite model search generation. The method SEM with and without both the function ordering and symmetry detection is experimented on several interesting mathematical problems to show the advantage of reasoning by symmetry and the function ordering.

12:00-12:30  Bernhard Gramlich, Vienna U of Techn., Austria
Reinhard Pichler, Vienna U of Techn., Austria
Algorithmic aspects of herbrand models represented by ground atoms with ground equations
Automated model building has evolved as an important subdiscipline of automated deduction over the past decade. One crucial issue in automated model building is the selection of an appropriate (finite) representation of (in general infinite) models. Quite a few such formalisms have been proposed in the literature. In this paper, we concentrate on the representation of Herbrand models by ground atoms with ground equations (GAE-models). For the actual work with any model representation, efficient algorithms for two decision problems are required, namely: The clause evaluation problem (i.e.: Given a clause C and a representation M of a model, does C evaluate to "true" in this model?) and the model equivalence problem (i.e.: Given two representations M1 and M2, do they represent the same model?). Previously published algorithms for these two problems in case of GAE-models require exponential time. We prove that the clause evaluation problem is indeed intractable (that is, coNP-complete), whereas the model equivalence problem can be solved in polynomial time. Moreover, we show how our new algorithm for the model equivalence problem can be used to transform an arbitrary GAE-model into an equivalent one with better computational properties.

Session 7

14:00-15:00  Daniel Jackson, Massachusetts Inst. of Techn., USA
Invited talk: Simple logic, complex systems

15:00-15:30  Lilia Georgieva, U Manchester, UK
Ullrich Hustadt, U Liverpool, UK
Renate A. Schmidt, U Manchester, UK
A new clausal class decidable by hyperresolution
In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.

Session 8: CASC

16:00-16:15  Christoph Weidenbach, Opel AG, Germany
Uwe Brahm, MPI Saarbrücken, Germany
Thomas Hillenbrand, MPI Saarbrücken, Germany
Enno Keen, MPI Saarbrücken, Germany
Christian Theobalt, MPI Saarbrücken, Germany
Dalibor Topic, MPI Saarbrücken, Germany
System description: SPASS version 2.0
SPASS is an automated theorem prover for full first-order logic with equality. This system description provides an overview of recent developments in SPASS 2.0, including among others an implementation of contextual rewriting, refinements of the clause normal form transformation, and enhancements of the inference engine.

16:15-16:30  Stephan Schulz, Techn. U of Munich, Germany
Geoff Sutcliffe, U Miami, USA
System description: System description: GrAnDe 1.0
The validity problem for full first-order logic is only semi-decidable. However, there are many interesting problems that, when expressed in clause normal form, have a finite Herbrand universe. They fall into a decidable subclass of first-order logic. Traditionally, such problems have been tackled using conventional first-order techniques. Some implementations, e.g. DCTP, are decision procedures for this class of problems. An alternative approach, justified by Herbrand's theorem, is to generate the ground instances of such a problem and use a propositional decision system to determine the satisfiability of the resulting propositional problem. The applicability of the grounding approach has led to these problems being called "effectively propositional" (EPR) problems. The TPTP problem library v2.4.1 contains 574 EPR problems. Many of these are group theory problems (101 problems) and CNF translations of formulae in propositional multi-modal logic (206 problems).

16:30-16:45  Simon Colton, U Edinburgh, UK
System description: System description: The HR program for theorem generation
Automated theory formation involves the production of objects of interest, concepts about those objects, conjectures relating the concepts and proofs of the conjectures. In group theory, for example, the objects of interest are the groups themselves, the concepts include element types, subgroup types, etc., the conjectures include implication and if-and-only-if conjectures and these become theorems if they are proved, non-theorems if disproved. Similar to Zhang's MCS program, the HR system - named after mathematicians Hardy and Ramanujan - performs theory formation in mathematical domains. It works by (i) using the MACE model generator to generate objects of interest from axiom sets (ii) performing the concept formation and conjecture making itself and (iii) using the Otter theorem prover to prove conjectures.

16:45-17:00  Michael Whalen, U Minnesota, USA
Johann Schumann, NASA Ames, USA
Bernd Fischer, NASA Ames, USA
System description: AutoBayes/CC - combining program synthesis with automatic code certification - system description
Our work combines code certification with automatic program synthesis which makes it possible to automatically generate both the code and all necessary annotations for fully automatic certification. By generating detailed annotations, one of the biggest obstacles for code certification is removed and it becomes possible to automatically check that synthesized programs obey the desired safety properties.

Herbrand award

17:00-17:10  Award ceremony

17:10-18:00  Mark Stickel, SRI International, USA
Acceptance speech: Title TBA

CASC (continued)

18:00-18:30  CASC results and discussion

19:30-22:00  Conference dinner

Room: Restaurant Luftkastellet