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:
No candidate reaches a majority right away,
and the redistribution of the votes of Bernhard Gramlich
yields the following new distribution:
Again, no candidate reaches a majority, and
by redistributing the votes of Gilles Dowek one gets the following table:
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:
None of the candidates has a majority to be elected,
so that the votes of Bernhard Gramlich need to be redistributed again:
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:
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)
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.
Many-valued logic (MV) can be defined (in clause form) with the following
five axioms.1
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
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,
and the following theorem in the implicational fragment of MV.
The implicational fragment of MV (MVI) is the sublogic defined by
the axioms {MV1, MV2, MV3, MV5}.
HR is known to be a single axiom for MVI, 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)
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 Proofi.
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
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,
Proof1
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
Proof1
as hints for this step.
We use OTTER to find this proof by including the positive form of
every negative clause appearing in Proof2.
For example, if -P(i(a,i(b,a)) appears in
Proof2, we include
P(i(x,i(y,x)) as a hint here.
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 Proof3, this is not necessarily the case, depending, for example,
on the types of inference steps permitted in Proof1.
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
Bibliography
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
The 18th International Conference on Automated Deduction
will take place in Copenhagen, Denmark, on
July 27-30, 2002.
Workshops and tutorial will be held
July 25, 26, and 31 and August 1, 2002.
Workshops and tutorials
will ordinarily run for one or two days, but half-day ones may be
possible as well.
Workshop Topics.
Recent CADE workshops have included term schematizations and their
applications, reasoning, automation of proofs by induction, empirical
studies in logic algorithms, mechanizations of partial functions,
proof search in type-theoretic languages, automated model building,
evaluation of automated theorem-proving systems, strategies in
automated deduction, automated theorem proving in software
engineering and in mathematics, and integration of symbolic computation
and deduction.
We encourage workshops that build on previous
events as well as new ones in novel research areas broadly
related to automation and deduction.
Tutorial Topics.
Recent CADE tutorials have included equality reasoning in semantic
tableaux, proof systems for nonmonotonic logics, rewrite techniques
in theorem proving, proof planning, parallelisation of deduction
strategies, resolution decision methods, constructive type theory,
the use of semantics in Herbrand-based proof procedures, logical
frameworks, theorem proving by the inverse method, deduction
methods based on boolean rings, higher-order equational logic, and
term indexing in automated reasoning.
Tutorials may be introductory, intermediate, or advanced. Tutorials
on novel research are also encouraged.
Proposals.
Anyone wishing to organize a workshop or tutorial in conjunction
with CADE-18 should send (e-mail preferred) a proposal (in ASCII
text format) no longer than two pages to the workshop/tutorial chair
and the program chair by October 12, 2001. The proposal
should describe the following:
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.
LICS 2002
The seventeenth annual IEEE Symposium on
Logic in Computer Science
will take place on July 22-25, 2002, in Copenhagen, Denmark,
as part of the 2002 Federated Logic Conference
(FLoC 2002).
Topics of interest for submissions
include automated deduction, categorical models and logics,
constraint programming, database theory, domain theory,
finite model theory, formal aspects of program analysis, formal
methods, lambda and combinatory calculi, linear logic,
logics in artificial intelligence, logics of programs,
logic programming, modal and
temporal logics, model checking, programming language semantics,
reasoning about security, rewriting,
type systems and type theory, and verification.
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.
CAV'02
The 14th International Conference on Computer Aided Verification
(CAV'02)
will be held in Copenhagen, Denmark, on July 27-31, 2002.
This year's CAV conference will be part of the Federation of Logic
Conferences.
Topics of interest include the following:
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
The
conference on Rewriting Techniques and Applications (RTA 2002)
will be held on
July 22-24, 2002,
in Copenhagen, Denmark,
as part of the Federated Logic Conference FLoC'02.
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.
FME2002
Formal Methods Europe (FME 2002)
will be held on July 20-24, 2002,
in conjunction
with the third Federated Logic Conference (FLoC'02) in Copenhagen, Denmark.
The theme of FME 2002 is Formal Methods: Getting IT Right.
The double meaning is intentional. On the one hand, the theme acknowledges
the significant contribution formal methods can make to Information
Technology, by enabling computer systems to be described precisely and
reasoned about with rigour. On the other hand, it recognises that current
formal methods are not perfect, and further research and practice are
required to improve their foundations, applicability and effectiveness.
FME seeks papers in all aspects of formal methods for computer systems,
including the following: theoretical foundations,
practical use and case studies,
specification and modeling techniques,
software development and refinement,
tool support and software engineering environments for formal methods,
verification and validation,
hidden formal methods, and making benefits available to nonexperts,
reusable domain theories, method integration, and hardware verification.
Full papers (max. 20 pages) should be
reach the Program Co-chairs by January 15, 2002.
Tutorials and workshops will be held on 20-21 July 2002. Each tutorial will
last one-half or one day. Proposals are welcome and should be directed to
the Program Co-chairs by January 15, 2002.
Tool demonstrations will also take place during the symposium, with the
opportunity for presentations to be made about each tool.
Proposals for
tool demonstrations should be made to the Tool Demonstration Coordinator,
with whom provison of necessary computing facilities should be discussed.
For details, please see the
Web site.
TABLEAUX 2002
A conference on
Automated Reasoning with Analytic Tableaux and Related Methods
will be held July 30-August 1, 2002,
at Copenhagen, Denmark (in the frame of FLoC 2002).
The conference brings together researchers interested in all
aspects of the mechanization of reasoning with
analytic tableaux and related methods.
Topics of particular interest include
analytic tableaux for various logics (theory and applications);
related techniques and concepts (e.g., model checking, BDDs);
related methods (model elimination, sequent calculi, connection
method, inverse method, etc.);
new calculi and deduction methods in classical
and nonclassical logics (description, modal, intuitionistic,
linear, temporal, etc.); and
systems, tools, implementations and applications (e.g., verification).
Submissions are invited in the following categories:
(A) full papers (experimental or theoretical research; up to 15 pages);
(B) system descriptions (up to 5 pages); and
(C) position papers and reports on work in progress (up to 15 pages).
Accepted papers of categories (A) and (B) will be published in
Springer's LNAI series. The proceedings will be available at the
conference. Accepted papers of category (C) will be available as a
technical report of the Vienna University of Technology and on the
Internet.
Submissions are due February 2, 2002.
For further information, please see the
Web site.
Results of the CADE Trustee Elections 2001
Maria Paola Bonacina
(Secretary of AAR and CADE)
E-mail: bonacina@cs.uiowa.edu
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
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
Candidate
1st Pref.
2nd Pref.
3rd Pref.
4th Pref.
Total
J. Harrison
60
59
3
1
123
F. Pfenning
61
58
2
2
123
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
Candidate
1st Pref.
2nd Pref.
3rd Pref.
4th Pref.
Total
G. Dowek
57
55
9
2
123
J. Harrison
65
52
6
0
123
Candidate
1st Pref.
2nd Pref.
3rd Pref.
4th Pref.
Total
G. Dowek
64
54
5
0
123
B. Gramlich
50
67
6
0
123
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)
A Strategy for Proving Theorems in Many-Valued Logic
Robert Veroff
E-mail: veroff@cs.unm.edu
-P(i(x,y)) | -P(x) | P(y).
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").
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").
% 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)))))).
% 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)).
K(x,y) = n(i(i(n(x),n(y)),n(y)))
EQ(i(i(t1,t2),x),x).
-P(i(x,y)) | -P(i(y,x)) | P(t[x],t[y]).
Note
1. MV5 is known to be dependent on
{MV1, MV2, MV3, MV4}.
Bibliography
Abstracts of Recent Ph.D. Theses in Automated Reasoning
The choice of the above logics was mainly dictated by the fact
that several problems of interest in the fields of knowledge
representation and formal verification can be naturally encoded
using propositional logic, or its modal and quantified superclasses.
Each system embeds both state-of-the-art techniques, and new ideas and
algorithms that were developed in the course of the thesis to improve
on the current available decision procedures in all the logics that we
review. As a result, SIM, *SAT and QuBE
compare favorably with
analogous systems from other researchers, and particularly:
SIM and QuBE homepages under Software Tools for Automated Reasoning (STAR) pages.
*SAT
homepage, including source code distribution, manual, papers and more.
[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 News
Call for Papers
The proceedings of the
conference will be published in the Springer-Verlag Lecture Notes
in Computer Science series.
Gail Pieper
2001-10-03