PaPS on Thursday

Detailed program
Thursday August 1st, 2002
See also the unified by-slot program

All sessions take place in auditorium 8.

Session 3

09:00-09:30  Jieh Hsiang, National Taiwan U, Taiwan
Yuh Pyng Shieh, National Taiwan U, Taiwan
YaoChinag Chen, National Taiwan U, Taiwan
The cyclic complete mapppings counting problems
A complete mapping of a group (G,+) is a permutation f(x) of G with f(0)=0 such that -x+f(x) is also a permutation of G. Given a group G, the Complete Mappings Counting Problem is to find, if any, the number of complete mappings of G. Complete mapping problems are ideal for testing the strength of propositional solvers. In this paper we describe various types of complete mapping problems, and their relationship with variations of the n-queen problems. We also present several forms of symmetry operators which, in addition to being theoretically interesting on their own, are crucial for improving the efficiency of the provers. Several classes of challenge problems for propositional provers are given, so are the transformations of these problems into propositional format.

09:30-10:00  John Slaney, Australian National U
A benchmark template for substructural logics
This paper suggests a benchmark template for non-classical propositional reasoning systems, based on work done some twenty years ago in the investigation of relevant logic. The idea is simple: generate non-equivalent binary operations in the language of the logic and use an automated rea- soning system to decide which ones satisfy given algebraic properties. Of course, problem classes generated in this way are not in any sense uniformly distributed: indeed, they are highly structured and have special features such as a low ratio of variables to length. Nonetheless, they have the character of theorem proving "in the field", and should be part of the evaluation equipment for systems dealing with a wide range of nonclassical logics.

10:00-10:30  Zac Ernst, U Wisconsin-Madison, USA
et al.
More first-order test problems in math and logic
This paper contains a collection of theorems, nontheorems, and conjectures in first-order and equational logic. These problems arose in our work on applications of automated deduction to mathematics and logic. Some originated in our work, and others were sent to us as challenge problems or open questions.

Session 4

11:00-11:30  Koen Claessen, Safelogic AB, Sweden
Reiner Hähnle, Chalmers U of Techn., Sweden
Johan Mårtensson, Safelogic AB, Sweden
Verification of hardware systems with first-order logic
The state of the art of automatic first order logic theorem provers is advanced enough to be useful in a commercial context. This paper describes a way in which first order logic and theorem provers are used at the Swedish formal verification company Safelogic, to formally verify properties of hardware systems. Two dirent verification methods are discussed, which both make use of translations of formalisms into first order logic. We draw some preliminary conclusions from our experiences and provide problems sets and benchmarks.

11:30-12:30  Johann Schumann, NASA Ames, USA
Invited talk: Using automated theorem provers? using automated theorem provers!
Automated theorem provers (ATPs) have gained tremendously in power over the last decade. However, when it comes to using them for a real application, the user will find out that they are not plug-and-play devices. Like race cars which are cool and fast on the race track but not good to shop for groceries around the corner, ATPs are in essence very efficient implementations of search algorithms. In this talk, I will report about experience of using ATPs for real-world applications like handling proof tasks in verification, certification, and software reuse. I will focus thereby on applications in safety-critical domains. In order to get an ATP running, a number of issues need to be considered carefully: (i) connecting the prover and converting the syntax of the formulas, (ii) getting the prover to work (axioms, conversion into CNF, sorts), (iii) getting results out of the prover (You want to hear more than "YES", don't you?), and (iv) reacting to failed proof attempts. In this talk, I will present several techniques which help resolving these issues and address the importance of common ATP support-tools and problem sets.