RDP                     
Home page
Organization
Sponsors

MEETINGS        
RTA
TLCA
FTP
WG1.6
RULE
UNIF
WFLP
WRS
WST

VENUE               
Valencia
Registration
Accomodation
Travelling
Program
Conference Venue
Internet
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