NEWSLETTER
No. 53, October 2001
Contents
From the AAR Presidnet
Results of the CADE Trustee Elections 2001
A Strategy for Proving Theorems in Many-Valued Logic
CADE-18
Call for Papers
Developing methods and software to help mathematicians, scientists, and engineers with the deductive aspects of their work -- this has long been and remains one of the goals of automated reasoning. I am pleased, therefore, to note that in this issue of the AAR Newsletter, we have two contributions that accomplish that goal. One contribution, by Robert Veroff, focuses on proving theorems in many-valued logic; the second contribution, by Armando Tacchella, focuses on the design and implementation of procedures for automated deduction in propositional and other logics. Both contributions report real success: in proving challenging theorems and in verifying real hardware designs.
An election was held from August 30 through September 15 to fill three positions on the board of trustees of CADE Inc. Two positions were left vacant by Claude Kirchner and Frank Pfenning, whose terms expired, and a third one was created to continue the implementation of the amendment approved in the summer of 2000 to increase the number of trustees from nine to twelve (see AAR Newsletters No. 48, August 2000, and No. 52, August 2001). Gilles Dowek, Bernhard Gramlich, John Harrison and Frank Pfenning were nominated for these positions.
Ballots were sent by electronic mail to all members of AAR as of August 30, for a total of 548 ballots (up from 445 in 2000 and 396 in 1999). Of these, 123 were returned with a vote, representing a participation level of 22.5% (down from 24.5% in 2000 and 30% in 1999). The majority is 50% of the votes plus 1, hence 62.
The following table reports the initial distribution of preferences among the four candidates:
Candidate | 1st Pref. | 2nd Pref. | 3rd Pref. | 4th Pref. | Total |
G. Dowek | 23 | 35 | 28 | 37 | 123 |
B. Gramlich | 20 | 23 | 28 | 52 | 123 |
J. Harrison | 43 | 21 | 31 | 28 | 123 |
F. Pfenning | 37 | 41 | 20 | 25 | 123 |
No candidate reaches a majority right away, and the redistribution of the votes of Bernhard Gramlich yields the following new distribution:
Candidate | 1st Pref. | 2nd Pref. | 3rd Pref. | 4th Pref. | Total |
G. Dowek | 34 | 35 | 45 | 9 | 123 |
J. Harrison | 48 | 29 | 42 | 4 | 123 |
F. Pfenning | 41 | 52 | 28 | 2 | 123 |
Again, no candidate reaches a majority, and by redistributing the votes of Gilles Dowek one gets the following table:
Candidate | 1st Pref. | 2nd Pref. | 3rd Pref. | 4th Pref. | Total |
J. Harrison | 60 | 59 | 3 | 1 | 123 |
F. Pfenning | 61 | 58 | 2 | 2 | 123 |
Thus, Frank Pfenning, current vice-president of CADE Inc., is re-elected for a second term on the board of trustees. (Since 61 is one vote short of the majority, the STV algorithm executes another round distributing the votes of John Harrison, but this is not reported because the outcome is obvious.) The redistribution of the votes of the winner produces the following table:
Candidate | 1st Pref. | 2nd Pref. | 3rd Pref. | 4th Pref. | Total |
G. Dowek | 39 | 43 | 37 | 4 | 123 |
B. Gramlich | 29 | 34 | 58 | 2 | 123 |
J. Harrison | 54 | 34 | 33 | 2 | 123 |
None of the candidates has a majority to be elected, so that the votes of Bernhard Gramlich need to be redistributed again:
Candidate | 1st Pref. | 2nd Pref. | 3rd Pref. | 4th Pref. | Total |
G. Dowek | 57 | 55 | 9 | 2 | 123 |
J. Harrison | 65 | 52 | 6 | 0 | 123 |
Thus, John Harrison has a majority and is elected. Returning to the table after Frank Pfenning's votes were redistributed, and redistributing those of John Harrison also, one obtains the following matrix:
Candidate | 1st Pref. | 2nd Pref. | 3rd Pref. | 4th Pref. | Total |
G. Dowek | 64 | 54 | 5 | 0 | 123 |
B. Gramlich | 50 | 67 | 6 | 0 | 123 |
so that Gilles Dowek has a majority and is elected.
After this election, the following people are serving on the board of trustees of CADE Inc.:
Maria Paola Bonacina (Secretary)
Gilles Dowek (Elected 9/2001)
Ulrich Furbach (President, elected 8/1997 and re-elected 10/2000)
Harald Ganzinger (Past program chair, elected 10/1999)
John Harrison (Elected 9/2001)
Michael Kohlhase (Elected 10/2000)
David McAllester (Past program chair, elected 10/2000)
Neil V. Murray (Treasurer)
Frank Pfenning (Vice-President, elected 10/1998 and re-elected 9/2001)
David A. Plaisted (Elected 10/1999)
Andrei Voronkov (Program Chair of CADE 2002)
On behalf of the AAR and CADE Inc., I thank Claude Kirchner, for his service as trustee during the past three years, Tobias Nipkow, for his service as program co-chair of IJCAR 2001 and ex-officio trustee, Bernhard Gramlich, for running in the election, all the members who voted, for their participation, and offer the warmest congratulations to Frank Pfenning, John Harrison and Gilles Dowek on being elected.
In this note, we outline a strategy that has worked quite well on a number of challenging problems in many-valued logic. The strategy is based on the use of proof sketches, first presented in [3].
Background
This work concerns the application of automated reasoning to logical systems based on the inference rule condensed detachment (CD). CD, which is a combination of modus ponens and universal instantiation, can be implemented in an automated reasoning system such as OTTER [1] by using hyperresolution and the following clause.
-P(i(x,y)) | -P(x) | P(y).
Many-valued logic (MV) can be defined (in clause form) with the following five axioms.^{1}
P(i(x,i(y,x))) # label("MV1"). P(i(i(x,y),i(i(y,z),i(x,z)))) # label("MV2"). P(i(i(i(x,y),y),i(i(y,x),x))) # label("MV3"). P(i(i(n(x),n(y)),i(y,x))) # label("MV4"). P(i(i(i(x,y),i(y,x)),i(y,x))) # label("MV5").
MV is a sublogic of two-valued logic (TV) in the sense that each of the axioms of MV is a theorem of TV. The Lukasiewicz system
P(i(i(x,y),i(i(y,z),i(x,z)))) # label("L1"). P(i(i(n(x),x),x)) # label("L2"). P(i(x,i(n(x),y))) # label("L3").
is one of several equivalent axiomatizations of TV. We exploit the relationship between MV and TV as part of our strategy.
The strategy described in this note relies on the generation and use of proof sketches, sets of clauses containing potentially key milestones on the way to a proof of a target theorem T. Operationally, the clauses appearing in a proof sketch are used as hints [2] to help guide the search for a proof of T. In particular, we put a bias in our search toward deduced clauses that back subsume such hint clauses.
We are especially interested in developing strategies for finding proof sketches that effectively lead to the proofs of target theorems. For example, one approach is to prove the target theorem with additional assumptions and then systematically eliminate these assumptions--using previous proofs as proof sketches--until a proper proof of the theorem is found.
Example Problems Solved
We recently have proved the following four distributivity theorems in MV,
% KA1: K distributes over A, direction 1 (KpAqr -> AKpqKpr) P(i(n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))), i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(z)),n(z)))), n(i(i(n(x),n(z)),n(z)))))). % KA2: K distributes over A, direction 2 (KpAqr <- AKpqKpr) P(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(z)),n(z)))), n(i(i(n(x),n(z)),n(z)))), n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))))). % AK1: A distributes over K, direction 1 (ApKqr -> KApqApr) P(i(i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))), n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))))). % AK2: A distributes over K, direction 2 (ApKqr <- KApqApr) P(i(n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))), i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))))).
and the following theorem in the implicational fragment of MV.
% HR: single axiom P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(i(z,u),i(i(v,z),i(v,u))), i(i(w,i(v6,w)),v7)),v7), i(i(i(i(v8,v9),v9),i(i(v9,v8),v8)),v10)),v10), i(i(i(i(v11,v12),i(v12,v11)),i(v12,v11)),v13)),v13), i(i(v14,i(v15,v14)),v16))),v16)).
The implicational fragment of MV (MV_{I}) is the sublogic defined by the axioms {MV1, MV2, MV3, MV5}. HR is known to be a single axiom for MV_{I}, but in this note we are concerned only with showing that it is a theorem.
The comments preceding the distributivity theorems refer to operators A and K. These operators are related, respectively, to our usual notions of logical disjunction (or) and conjunction (and) and are defined as follows.
A(x,y) = i(i(x,y),y)
K(x,y) = n(i(i(n(x),n(y)),n(y)))
You can read more about these theorems and see their proofs on the Web.
The significance of these theorems for this short note is simply that they appear to be especially difficult to prove with OTTER. One reason is that they are fairly long formulas when compared with the lengths of the axioms; the HR single axiom, for example, has length 70. OTTER tends to work better when its search can be restricted to shorter formulas.
A Strategy
Here is a rough outline of a strategy for proving a theorem T in many-valued logic (or in some related logic). The basic idea is that the proof or proofs found for each step can be used as proof sketches to help guide the search in the later steps. We note that some of these steps are nontrivial and present interesting challenges themselves. We will discuss some of these issues in more detail in a future article.
Each step i results in a proof (or set of proofs), which we will denote Proof_{i}.
Finding a proof in TV often is substantially easier than finding a proof in MV. Although a proof in TV is not necessarily a proof in MV, given the close tie between the two logics, the TV proof may tell us a lot about what to look for in an MV proof, for example, if it contains steps that are theorems in MV.
Finding a TV proof may involve using several of the techniques described in [3], for example, relying on heuristics that include the use of paramodulation and demodulation and permitting applications of inferences rules to the clause representing the denial of the theorem and to its descendants.
Although there are known substitution properties for TV, at this point we may relax things even further by permitting in addition certain paramodulation steps that may not be sound even in TV. For example, we may permit paramodulations from clauses of the form
EQ(i(i(t1,t2),x),x).
when P(i(t1,t2)) is known to be a theorem, even though P(i(t2,t1)) may not be a theorem. As a consequence, Proof_{1} may contain steps that are not theorems in TV. Nevertheless, finding such a proof has proven to be a useful starting point for our searches.
We use OTTER to find this proof by including all of the intermediate demodulants used in Proof_{1} as hints for this step.
We use OTTER to find this proof by including the positive form of every negative clause appearing in Proof_{2}. For example, if -P(i(a,i(b,a)) appears in Proof_{2}, we include P(i(x,i(y,x)) as a hint here.
-P(i(x,y)) | -P(i(y,x)) | P(t[x],t[y]).
where t[x] is a term with exactly one occurrence of the variable symbol x, and t[y] is the same term but with variable symbol y instead of x. Note that a hyperresolvent resulting from such a clause characterizes a type of substitution property when used as the major premise in an application of CD. We'll refer to such a clause as a substitution theorem.
Although it may appear that a sufficient set of substitution theorems can be determined directly from the paramodulation steps in Proof_{3}, this is not necessarily the case, depending, for example, on the types of inference steps permitted in Proof_{1}.
Although we could implement a special procedure for this step, we have been successful at using OTTER to find these derivations.
As we indicated, some of these individual steps can be challenging. It took us several weeks to find the proof of theorem KA2, and the proof we found is 140 steps long. On the other hand, we found a CD derivation of theorem HR two days after we were presented the problem.
Author: Armando Tacchella
Advisor: Proff. Enrico Giunchiglia and Mauro Di Manzo
Defense date: February 2001
Institution: Dipartimento di Informatica, Sistemistica e Telematica, Università degli Studi di Genova, Italia
Abstract: This work focuses on the development of computer procedures for automated deduction in the following logics:
The contribution of this thesis is the design, the implementation and the experimental testing of three systems:
The systems that we developed are interesting not only from the research perspective, but also from an application point of view. SIM is at the heart of two technology-transfer projects. The first one is THUNDER, an open architecture for SAT-based verification of hardware designs developed by the Logic Validation Technologies Group at the Israel Development Center of Intel Corp. An object oriented version of SIM (SIMO) has been recently integrated into THUNDER and used to debug the design of some Pentium IV components. THUNDER(SIMO) outperforms other traditional validation technologies [CF+01]. The second technology transfer project centered around SIM is in cooperation with Istituto per la Ricerca Scientifica e Tecnologica (IRST-ITC) in Trento and involves the integration of SIM into the NuSMV [CC+98] model checker, a tool for debugging and verifying hardware designs and software protocols.
On-line resources
SIM and QuBE homepages under Software Tools for Automated Reasoning (STAR) pages.
*SAT
homepage, including source code distribution, manual, papers and more.
Bibliography
[BS97] R. J. Bayardo Jr. and R. C. Schrag.
Using CSP Look-Back Techniques to Solve Real-World SAT instances.
In Proc. of AAAI, pages 203-208. AAAI Press, 1997.
[CC+98] A. Cimatti, E. Clarke, F. Giunchiglia and M. Roveri.
NuSMV: A new symbolic model checker.
Journal on Software Tools for Technology Transfer, 2:4,
pages 410-425, Springer Verlag, 2000.
[CF+01] F. Copty, L. Fix, Ranan Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella and M. Y. Vardi.
Benefits of bounded model checking at an industrial setting.
In Proc. of CAV, 2001.
[CGS98] M. Cadoli, A. Giovanardi, and M. Schaerf.
An algorithm to evaluate quantified boolean formulae.
In Proc. of AAAI, 1998.
[Fre95] J. W. Freeman.
Improvements to propositional satisfiability search algorithms.
Ph.D. thesis, University of Pennsylvania, 1995 .
[Hor97] I. Horrocks.
Optimizing tableaux decision procedures for description logics.
Ph.D. thesis, University of Manchester, 1997.
[HS97] U. Hustadt and R. A. Schmidt.
On evaluating decision procedures for modal logic.
In Proc. of IJCAI, 1997.
[LA97] C. M. Li and Anbulagan.
Heuristics based on unit propagation for satisfiability problems.
In Proc. of IJCAI, pages 366--371. Morgan-Kauffmann, 1997.
[PS98] P. F. Patel-Schneider.
DLP system description.
In Collected Papers from the International Description Logics
Workshop (DL'98). CEUR Workshop Proceedings, 1998.
[Zha97] H. Zhang.
SATO: An efficient propositional prover.
In Proc. of CADE, volume 1249 of LNAI, pages 272--275.
Springer Verlag, 1997.
CADE-18 Call for Papers
The Conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974. Early CADEs were mostly biennial; annual conferences have been held since 1996. In 2001, CADE, TABLEAUX, and FTP merged into one conference called the International Joint Conference on Automated Reasoning (IJCAR). This year CADE-18 is a participant of the Federated Logic Conference (FLoC'02), which will be held in Copenhagen, Denmark, July 27-30, 2002.
CADE-18 invites submissions related to all aspects of automated deduction, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited.
Logics of interest include propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, type theory and set theory.
Techniques of interest include induction, term rewriting, constraint solving, satisfiability checking, model checking, resolution, semantic tableaux, sequent calculi, model-elimination, inverse method, interactive theorem proving, proof planning, term indexing, implementation techniques, decision procedures, unification, model generation, semantic guidance, logical frameworks, proof presentation.
Applications of interest include verification, formal methods, program analysis and synthesis, declarative programming, proof carrying code, deductive databases, knowledge representation, computer mathematics, natural language processing, linguistics, robotics, planning.
There are three categories of submission: (A) regular papers (max. 15 pages), (B) experimental papers (max. 10 pages), and (C) system descriptions (max. 5 pages) accompanied by a demonstration. The proceedings of CADE-18 will be published by Springer-Verlag in the LNAI/LNCS series. All submissions must be received by February 2, 2002. Details about paper preparation are in the Web site. Details about CADE-18 are available on the Web site.
As in previous CADEs, an Automated Theorem Prover System Competition will be held at CADE-18.
CADE-18 Call for Workshops and Tutorials
Proposals will be evaluated, and decisions will be communicated by October 26, 2001. Further information about the arrangements for workshops and tutorials can be obtained from the CADE-18 Web site.
The deadline for submissions is January 15, 2002. For further information, see the Web site.
LICS 2002 will have a session of short (5-10 minutes) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages), should be entered at the LICS submission site March 25-29, 2002.
Other events: The following conferences will participate at FLoC 2002: CADE, CAV, FME, ICLP, RTA, TABLEAUX; see the Web site for details. There will also be many workshops sponsored by the FLoC conferences. For details about the LICS workshops, see the Web site.
There are two categories of submissions: (A) regular papers (max. 13 pages); and (B) tool presentations (max. 4 pages). Paper submissions are due January 15, 2002. For further details, see the conference home page.
RTA 2002 solicits original papers on all aspects of rewriting, including applications, foundations, frameworks, implementations, semantics. There are four submission categories: (1) regular research papers describing new results, (2) papers describing the experience of applying rewriting techniques in other areas, (3) problem sets that provide realistic and interesting challenges in the field of rewriting, and (4) system descriptions. Submissions must reach the program chairperson by January 15, 2002. Please see the Web site for further information.
For details, please see the Web site.
Submissions are due February 2, 2002. For further information, please see the Web site.