 | |
Sessions
take place in auditorium 3 unless otherwise indicated.All-day activities| 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. |
| 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. |
| 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. |
| 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. |
| 17:00- | 17:10
| Award
ceremony |
| 17:10- | 18:00
| Mark Stickel, SRI International, USA
Acceptance
speech: Title TBA |
| 18:00- | 18:30
| CASC
results and discussion |
Room:
Restaurant Luftkastellet | |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
