RDP
MEETINGS
VENUE
|
FTP'03
|
4th International Workshop on First order Theorem Proving
Valencia, Spain, June 12-14, 2003
|
ABSTRACTS OF INVITED TALKS
SAT and Beyond SAT
|
Enrico Giunchiglia
(DIST Department, University of Genova, Italy)
|
In the last few years we have seen a tremendous boost in the
performance and capacity of SAT solvers, both on randomly
generated instances and on instances coming from real-world
problems. This boost has fostered the solution of real-world
problems via compilation to SAT and/or via the construction of
SAT-based engines.
In this talk, I will first survey the state-of-the-art on SAT
solvers technology (possibly reporting also on the results of
the last SAT competition), and then I will discuss how it is
possible to define SAT-based decision procedures for more
expressive formalisms.
|
Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
|
Thomas Hillenbrand
(Max-Planck-Institut für Informatik, Saarbrücken, Germany)
|
In the last years, the development of automated theorem provers has been
advancing in a so to speak Olympic spirit, following the motto "faster,
higher, stronger"; and the WALDMEISTER system has been a part of that
endeavour. We will survey the concepts underlying this prover, which
implements Knuth-Bendix completion in its unfailing variant. The system
architecture is based on a strict separation of active and passive
facts, and is realized via specifically tailored representations for
each of the central data structures: indexing for the active facts,
set-based compression for the passive facts, successor sets for the
hypotheses. In order to cope with large search spaces, specialized
redundancy criteria are employed, and the empirically gained control
knowledge is integrated to ease the use of the system. We conclude with
a discussion of strengths and weaknesses, and a view of future
prospects.
|
Deduction as an Engineering Science
|
Dieter Hutter
(DFKI GmbH, Saarbrücken, Germany)
|
Although in recent years a considerable progress has been made
in the theory of automated theorem proving, the use of theorem
provers in practice is still more or less restricted to a
limited number of academic groups. A lot of effort has been
spent in techniques to optimize the underlying logic engine
by, for instance, developing efficient datastructures or
controlling redundancy in large search spaces. However, the
development of techniques and methodologies to integrate such
a logic engine into an overall proof assistant has gained less
attraction. In this abstract we discuss the related research
problems briefly and will explore possible ways to tackle
these problems in the extended version of this paper.
|
Last update May 2003 # sescobar@dsic.upv.es
|