| | All
sessions take place in auditorium 8.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. |
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. |
| |