From the AAR President, Larry Wos...
Thanks to Maria Paola Bonacina's encouragement, we are beginning to hear from new Ph.D. graduates in automated reasoning. In this issue we include abstracts of three recent doctoral theses. I hope to hear more from these researchers soon.
In this regard, I am delighted to include an article by a Ph.D. student, Branden Fitelson, on finding "proofs within proofs" and then--so dear to my heart--"elegantizing" the proofs. In his article, Fitelson mentions the so-called Sheffer stroke, for which a number of simplifications have been published. Also in this issue of the AAR Newsletter, Robert Veroff reports on his current research on the Sheffer stroke, work that he is doing in collaboration with several colleagues including Fitelson.
Finally, I am pleased to announce that Bill McCune has won the Herbrand Award for the year 2000. He is indeed a fine researcher and a superb colleague.
1. Introduction
In the present note, I look at a famous historical example of DS proofs
that is nontrivial to convert into a CD proof. I also discuss how
OTTER can be used to perform the translation and to help one find the
shortest CD proof containing all the formulas in a known DS proof.
2. An Example: A
What we want is a CD proof containing all of the 28 steps of
In the APPENDIX is an OTTER input file that
implements this basic proof-finding strategy. Using this basic input file,
OTTER finds a proof in just a few minutes. The first proof it finds
contains 47 CD steps.
Once a proof is found, the process of elegantization begins. Larry Wos
and I have developed many strategies for aiding the search for elegant proofs in
formal logic [7, 6, 9, 1]. Using these strategies, we have
been able to find a 36-step CD proof that contains all 28 of
I leave it as a challenge problem
for AAR newsletter readers to try to improve on our 36-step CD completion of
Some Other Historical Examples
Mordchaj Wajsberg was a student of
Appendix
Basic OTTER Input File for
36-Step CD Proof Containing
[2] J. Kalman.
Condensed detachment as a rule of inference.
Studia Logica, 42:443-451, 1983.
[3] J.
[4] R. Veroff.
Using hints to increase the effectiveness of an automated reasoning
program: Case studies.
Journal of Automated Reasoning, 16(3):223-239, 1996.
[5] M. Wajsberg.
Logical Works.
Polish Academy of Sciences,
Wroc
[6] L. Wos.
Automating the search for elegant proofs.
Journal of Automated Reasoning, 21(2):135-175, 1998.
[7] L. Wos.
The Automation of Reasoning: An Experimenter's Notebook with
OTTER Tutorial.
Academic Press, 1996.
[8] L. Wos.
Conquering the Meredith single axiom.
Preprint ANL/MCS/P815-0500. Mathematics and Computer Science Division,
Argonne National Laboratory.
[9] L. Wos.
A Fascinating Country in the World of Computing: Your Guide to
Automated Reasoning.
World Scientific, 1999.
[10] L. Wos.
The resonance strategy.
Computers and Mathematics with Applications, 29(2):133-178,
1995.
[11] L. Wos with G. W. Pieper.
The hot list strategy.
Journal of Automated Reasoning, 22(1):1-44, 1999.
My colleagues and I are using Otter to find short bases
for Boolean algebra in terms of the Sheffer stroke.
An ongoing report of this work is available on the
Web page.
In the last issue of the AAR newsletter, we initiated
a new section featuring abstracts of recent doctoral dissertations in automated deduction and theorem proving.
This time we have three abstracts to include.
1. Title: Superposition Theorem Proving for Commutative Algebraic Theories
Author: Jürgen Stuber
Advisor: Harald Ganzinger
Defense date: June 2000
Institution: Max-Planck-Institute for Computer Science, Saarbrücken, Germany
Abstract:
We develop special superposition calculi for first-order
theorem proving in the theories of Abelian groups,
commutative rings, and modules and commutative algebras
over fields or over the ring of integers,
in order to make automated theorem proving in these theories more effective.
The calculi are refutationally complete
on arbitrary sets of ground clauses,
which in particular may contain additional function symbols.
The ground calculi are derived systematically from a representation
of the theory as a convergent term rewriting system.
Compared wuth standard superposition, they have stronger ordering restrictions
so that inferences are applied only to maximal summands,
and they contain macro inference rules
that use theory axioms in a goal directed fashion.
In general we need additional inferences to handle critical peaks
between extended clauses.
We show that these are not needed for Abelian groups and modules,
and that for commutative rings and commutative algebras
one such inference suffices for any pair of ground clauses.
To facilitate the construction of term orderings for such calculi,
we introduce theory path orderings.
2. Title:
Reasoning about Terminating Functional Programs
Advisor: Tobias Nipkow
Author: Konrad Slind
Institution: Institut für Informatik, Technische Universität München
Defense date: November 15, 1999
Abstract:
This thesis addresses two basic problems with the current crop of
mechanized proof systems. The first problem is largely technical: the
act of soundly introducing a recursive definition is not as simple and
direct as it should be. The second problem is largely social: there is
very little code-sharing between theorem prover implementations; as a
result, common facilities are typically built anew in each proof system,
and the overall progress of the field is thereby hampered.
We use the application domain of functional programming to explore the
first problem. We build a pattern-matching style recursive function
definition facility, based on mechanically proven well-founded recursion
and induction theorems. Reasoning support is embodied by automatically
derived induction theorems, which are customized to the recursion
structure of definitions. This provides a powerful, guaranteed sound,
definition-and-reasoning facility for functions that strongly resemble
programs in languages such as ML or Haskell. We demonstrate this package
(called TFL) on several well-known challenge problems.
In spite of its power, the approach suffers from a low level of
automation, because a termination relation must be supplied at function
definition time. If humans are to be largely relieved of the task of
proving termination, it must be possible for the act of defining a
recursive function to be completely separate from the act of finding a
termination relation for it and proving the ensuing termination
conditions. We show how this separation can be achieved, while still
preserving soundness. Building on this, we present a new way to define
program schemes and prove high-level program transformations.
Since the second problem is largely social, we cannot solve it alone;
however, we do present an artifact that marks a path to a brighter
future. In particular, we show that the sophisticated algorithms
implemented in TFL can be parameterized by a higher order logic
proof system. The package has been instantiated to HOL and Isabelle-HOL,
two quite different mechanizations of higher order logic. In this
exercise, we found that the fully formal approach taken to justifying
definitions and deriving induction schemes was fundamental in providing
the required combination of portability and soundness.
Current Address:
University of Cambridge Computer Laboratory,
New Museums Site, Pembroke Street,
Cambridge CB2 3QG, United Kingdom.
E-mail Address: kxs@cl.cam.ac.uk
3. Title:
Soft Typing for Clausal Inference Systems
Author:
Christoph Meyer
Advisor:
Prof. H. Ganzinger, MPI, Saarbrücken
Institution:
University of Saarbrücken, Germany, 1999
Abstract:
The purpose
of this thesis is to study methods for the semantical
control of automated theorem proving systems for first-order logic
(with equality) based on certain effective abstraction techniques. We
propose a general framework called soft typing for clausal inference
systems to incorporate the validity/satisfiability of clauses with
respect to certain model hypotheses into the control of inference
systems. The effectiveness of the method is obtained by inferring
automatically abstractions that result in approximations of
validity/satisfiability of clauses with respect to these models. For
an effective use of soft typing for ordered resolution and
superposition, we propose the use of sets of Horn clauses (with
equality) to represent approximations of model hypotheses for sets of
clauses. We show that certain decidable fragments of first-order
logic without equality can be generalized to non-trivial decidable
(equational) fragments. The satisfiability of clauses with respect to
the approximations implies the satisfiability in the original model
hypotheses.
See the
Web site for the full version.
Searchable Index for the Journal of Automated Reasoning
The Journal of Automated Reasoning
now has online an index of all the articles since its founding
in 1985.
Included are keywords,
which researchers may find useful in locating an article relevant
to their studies.
The information is available from the
JAR Web page.
We remind readers that the Journal is available
to AAR members
at a dramatically reduced price: $79 instead of the regular $242.
Special Issue of JSC on Rings
The deadline for submission to the special issue of the
Journal of Symbolic Computation on "Effective Methods in Rings of
Differential Operators"
has been extended
to October 15, 2000.
For more details see the
Web page.
Special Issue of JSC on First-Order Theorem Proving
A special issue of the
Journal of Symbolic Computation will be edited to commemorate the
recent success of FTP 2000, the third workshop
on First-Order Theorem Proving.
Like FTP 2000 itself, the special issue will focus on first-order
theorem proving as a core theme of automated deduction.
The editors of this special issue,
Peter Baumgartner and Hantao Zhang, welcome original,
unpublished contributions;
contributions are not limited to those presented at FTP 2000.
Submissions should be sent by e-mail in Postscript format to
ftp00@cs.uiowa.edu, accompanied by a plain text abstract.
The deadline is October 1, 2000.
William McCune has been named recipient of the Herbrand Award for the year 2000.
The award is given by Conference on Automated Deduction (CADE) Inc. to honor exceptional contributions to the
field of automated deduction.
McCune is a senior scientist in the Mathematics and Computer Science
Division at Argonne National Laboratory. He was cited for his outstanding success in answering the
Robbins question, which had challenged mathematicians and logicians for six decades, and for his
design of the powerful program OTTER, which has become a benchmark for automated deduction
programs.
McCune's contributions to the field also include powerful inference rules and numerous new strategies that have dramatically increased the likelihood of finding a proof.
Indeed, McCune has answered numerous open questions in such diverse areas as combinatory logic, group theory, algebra, and
logic calculi.
The Herbrand Award was presented at the CADE-17 in June 2000 in Pittsburgh.
1. Amendment to the CADE Inc. Bylaws
The following amendment to the CADE Inc.
bylaws
was proposed by David Plaisted,
and approved at the Business Meeting of CADE-17 with strong support.
A ballot to vote on this amendment was
distributed to the membership on July 6 with time to vote until
August 31, 2000.
Proposed Amendment to the CADE Bylaws, by David A. Plaisted
The following amendment to the bylaws of CADE passed with an
overwhelming majority at the CADE 2000 business meeting, and is
now being put to a vote of the entire membership of the AAR:
The number of trustees elected following each CADE conference will
be increased from two to three, while maintaining their term at
three CADE conferences, normally three years.
This means that
there will be a total of nine elected trustees instead of six.
The number of elected trustees is currently six, and will increase
by one at each trustee election following CADE 2000 until the
total reaches nine.
For an amendment to pass, at least 30\% of the AAR
membership must vote on it, and of those voting, at least two
thirds must vote in favor.
Therefore every vote matters, and your vote is very important.
Justification of the Proposed Amendment, by David A. Plaisted
In every trustee election so far, there have been more than two
qualified candidates, and there is no reason why a third candidate
cannot serve as a trustee.
CADE is facing some challenges and opportunities now. Three more
bright and qualified trustees would be a significant help in
meeting these.
This amendment would make it easier to elect trustees from areas
such as AI and hardware verification, and thereby broaden the
scope and appeal of CADE.
Currently there are three ex officio trustees who are appointed
but not elected, namely, the secretary, the treasurer, and the
upcoming program chair. There are also six elected trustees.
This amendment would make CADE more democratic, since roughly 3/4
of the trustees would be elected instead of 2/3 as at present.
This would give you, the members of the AAR, a greater voice in CADE.
2. Upcoming CADE Trustee Elections
The following people are currently serving as Trustees of CADE Inc.:
Ulrich Furbach, President (Elected 8/1997)
The terms of Ulrich Furbach and William McCune are expiring,
leaving two positions to be filled.
If the above amendment is approved, it will be implemented by introducing
a new position for three consecutive elections.
For instance, at the next election, there will be three, rather than two,
open positions.
The following candidates were nominated for the next CADE Trustee elections:
Ulrich Furbach
All AAR members will receive a ballot for this election.
The Office of Naval Research invites researchers to submit white papers
and proposals on the topic of
Digital Libraries for Constructive Mathematical Knowledge.
The objective is to create a digital library of algorithms and constructive mathematics usable for program and software construction.
Among the research concentration areas listed is proof-checking and model checking for certifying proofs of the standard body of
computationally related mathematics.
White papers (6 pages or less) are due August 17, 2000.
For further information, see the
Web page.
FLoC'02
The third Federated Logic Conference (FLoC'02)
will be held in Copenhagen, Denmark, July 20 - August 1, 2002.
Pre-conference workshops will be held on July 20-21.
Three conferences will be held in parallel during July 22-25:
Calls for papers and call for workshop proposals will be issued in the near
future. For additional information regarding the participating meetings,
please check the
FLoC Web page later this fall.
LICS
The sixteenth annual IEEE Symposium on
Logic in Computer Science will be held on
June 16-19, 2001, in Boston, Massachusetts.
LICS is an annual international forum on theoretical and
practical topics in computer science that relate to logic in a broad
sense.
Suggested topics of interest for paper submissions
include abstract data types, automata theory, automated deduction,
categorical models and logics, concurrency and distributed
computation, constraint programming, constructive mathematics,
logic in databases, domain theory, finite model theory, formal aspects of
program analysis, formal methods, hybrid systems, lambda and
combinatory calculi, linear logic, logical aspects of computational
complexity, logics in artificial intelligence, logics of programs,
logic programming, modal and temporal logics, model checking,
programming language semantics, reasoning about security, rewriting,
specifications, type systems and type theory, and verification.
The deadline for submissions is January 8, 2001.
LICS 2001 also will have a session of short (5-10 minute) 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)
will be due
March 31, 2001.
Researchers and practitioners also are invited to submit proposals for
workshops.
Proposals should consist of two parts. First, a short scientific
justification of the proposed topic, its significance, and the
particular benefits of a workshop. A second, organizational, part
should include
contact information for organizers;
proposed format and agenda;
procedures for selecting papers and participants;
and duration and preferred period (pre- or post-LICS).
Proposals are due October 1, 2000, and should be sent to
Leonid Libkin, e-mail: libkin@research.bell-labs.com.
For further information, see
the
LICS Web site
for details.
ACL2 Workshop 2000
The next workshop on the ACL2 theorem prover and its applications will
be held at the University of Texas on Monday and Tuesday, October
30-31, 2000. Immediately after the ACL2 workshop, Austin will host the
Formal Methods in Computer-Aided Design (FMCAD) conference. It will
be easy to attend both.
This year's ACL2 workshop is open to all.
For those who don't know ACL2 but wish to learn enough to listen to
the talks and see what's going on in the ACL2 community, we will
present a brief tutorial on Sunday afternoon,
October 29,
before the meeting.
There will be a nominal registration fee to cover the cost of food,
the meeting room, and (we expect) the proceedings, to be produced and
mailed after the meeting. We anticipate the fee being around $100
and will give full details when the details have been finalized.
The fee will be collected by check or cash at the workshop.
For details, see the
Web site.
IJCAR
The International Joint Conference on Automated Reasoning (IJCAR) is
the fusion of three major conferences in Automated Reasoning: CADE
(International Conference on Automated Deduction), TABLEAUX (international
conference on automated reasoning with analytic tableaux
and related methods), and FTP (international workshop on
First-Order Theorem Proving). These three events will join for the
first time at the IJCAR conference in Siena in June 2001.
Research papers.
IJCAR 2001 invites submissions related to all aspects of automated
reasoning, including foundations, implementations, and
applications. Original research papers (up to 15 pages)
and descriptions of working
automated deduction systems (up to 5 pages) are solicited.
All submissions must be received by January 14, 2001.
Note:
A prize of 500 Euros will be given to the best paper, as judged by the
program committee, written solely by one or more full-time students.
Short papers (up to 10 pages) are also solicited.
These are intended for quick dissemination of work in progress
or results not substantial enough for a full research paper.
Authors of accepted papers are expected to present a brief outline
of their work at the conference
and to prepare a poster for display at the conference venue.
The submission deadline is April 2, 2001.
Tutorials.
Proposals (1-2 pages) for tutorials are also solicited.
At present, the tutorials are
scheduled to take place on June 18-19.
The deadline for submission of is January 15, 2001.
Workshops.
Researchers and practitioners are invited to submit proposals
(2 pages)
for workshops on IJCAR-related topics.
Workshops that close the gap between automated
reasoning and related areas -- for instance, formal methods or
software engineering -- are especially encouraged.
The deadline for submission is January 1, 2001.
For details, see the
Web site.
RTA
The 12th International Conference on Rewriting Techniques and Applications
will take place on May 22-24, 2001, at
the Sea of Galilee, Israel.
Papers are solicited on
all aspects of rewriting, including applications, foundations,
frameworks, implementation, and semantics.
Submissions should fall into one of the following categories:
(1) regular research papers describing new results, judged
on correctness and significance (15 pages);
(2) papers describing the experience of applying rewriting techniques in
other areas, judged on relevance and comparison with
other approaches (15 pages);
(3) problem sets that provide realistic and interesting challenges in
the field of rewriting (15 pages); and
(4) system descriptions, containing a link to a working system to be
judged on usefulness and design (4 pages).
Note: A prize of 2001 NIS will be given to the best paper as judged by the
program committee.
For details about the conference and submissions, see
the
Web site.
Proofs within Proofs
Branden Fitelson
University of Wisconsin-Madison (fitelson@students.wisc.edu)
If one surveys the logical literature, one will find more than a few examples of
proofs that are less than fully rigorous from an axiomatic point of view. In
particular, one will find many proofs in which detachment plus substitution (DS)
is used instead of pure condensed detachment (CD). While it is known that any
theorem provable with DS is provable with CD (and vice versa1), it is not always easy to turn a DS proof into a CD proof.
Sometimes we get lucky and a known DS proof is already a CD proof. But,
usually, DS proofs contain gaps. Filling these gaps in DS proofs often requires
several CD steps. As such, it is useful to think of DS proofs as incomplete
"proof sketches'' that must be completed. When a DS proof sketch is turned
into a complete CD proof, the resulting CD proof will contain the DS proof
sketch as a "proof within a proof''.
ukasiewicz Single Axiom
ukasiewicz [3, pages 299-300] reports a 28-step DS proof
sketch of the three Tarski-Bernays axioms for classical, two-valued implication
from his (shortest) implicational single axiom. Some of the steps of
ukasiewicz's DS proof sketch are correct from a CD point of view. But,
several of the steps require less than most general
instantiations (i.e., unifications).
So, these steps
are really gaps, from a CD point of view.
ukasiewicz's DS
proof sketch. In fact, we'd like to find the shortest such proof. This
is where OTTER comes in. We can very efficiently search for the
desired proof by using the following three OTTER tricks:
ukasiewicz's DS proof sketch in the usable
list. This tells OTTER to stop only when it has found a proof
that contains all of the 28 steps in ukasiewicz's DS proof
sketch (i.e., a refutation of all 28 denials).2
ukasiewicz's DS proof sketch either in the
hints list or in a weight_list (or both), to be given a
low weight either as hints [4] or as resonators [10] (or
both). This tells OTTER to key on ukasiewicz's steps
during the search, thereby leading OTTER to the desired proof as
quickly as possible. I have found that, when trying to fill gaps in DS
proofs, using both resonators and hints is most effective.
ukasiewicz's single axiom (plus CD) in
the hot list. The hot list strategy [11] is very effective
in single axiom problems for filling gaps (and for finding proofs in
general). I have found that setting the heat parameter even as
high as 8 or more can greatly speed OTTER's finding of proofs
from single axioms (see also [8]).
ukasiewicz's
DS proof sketch steps (included in the APPENDIX). This is the shortest
such proof we have been able to find.
ukasiewicz's 28-step DS proof sketch.
ukasiewicz. In his master's
thesis, Wajsberg reports several DS proofs that contain many large gaps,
from a CD point of view. In particular, [5, pages 192-195]
reports DS proofs of three axiomatizations for the implicational fragment
of classical two-valued sentential logic. Each of these proofs contains
several rather large gaps, from a CD point of view. Wajsberg also reports
DS proof sketches for four axiomatizations of the equivalential calculus
[5, pages 195-198], as well as an axiomatization of two-valued
logic, based on Sheffer's stroke [5, pages 37-38].
ukasiewicz Problem
set(hyper_res).
assign(max_weight, 32).
assign(max_distinct_vars, 8).
assign(heat,2).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
set(order_history).
set(input_sos_first).
assign(bsub_hint_wt, 1).
set(keep_hint_subsumers).
list(hints).
% Following is Lukasiewicz's 28 step DS proof sketch (as hints)
P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(x,i(y,u)))).
P(i(i(i(x,i(y,z)),i(i(x,y),i(u,y))),i(v,i(i(x,y),i(u,y))))).
P(i(i(i(x,y),x),i(z,x))).
P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))).
P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))).
P(i(i(i(x,i(y,z)),i(u,i(z,v))),i(w,i(u,i(z,v))))).
P(i(i(i(x,y),z),i(y,z))).
P(i(x,i(i(x,y),i(z,y)))).
P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))).
P(i(i(i(x,y),i(i(i(y,z),u),i(v,u))),i(w,i(i(i(y,z),u),i(v,u))))).
P(i(i(i(x,i(i(i(y,z),u),i(v,u))),i(w,y)),i(v6,i(w,y)))).
P(i(i(i(x,i(y,z)),i(u,i(i(i(z,v),w),i(v6,w)))),i(v7,i(u,i(i(i(z,v),w),i(v6,w)))))).
P(i(i(i(x,y),i(z,u)),i(i(i(y,v),u),i(z,u)))).
P(i(i(i(x,y),i(z,u)),i(i(x,u),i(z,u)))).
P(i(i(x,i(y,z)),i(i(i(x,u),z),i(y,z)))).
P(i(i(i(i(i(x,y),z),u),i(v,x)),i(i(z,x),i(v,x)))).
P(i(i(i(i(x,y),i(z,y)),i(i(i(y,u),x),v)),i(w,i(i(i(y,u),x),v)))).
P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,z),u),i(x,y)))).
P(i(i(i(i(x,y),y),i(z,y)),i(i(i(y,u),x),i(z,y)))).
P(i(i(i(i(x,y),z),z),i(i(z,y),i(x,y)))).
P(i(x,x)).
P(i(i(i(x,y),z),i(i(z,x),x))).
P(i(x,i(i(x,y),y))).
P(i(i(x,y),i(i(i(x,z),y),y))).
P(i(i(i(i(x,y),i(i(y,z),i(x,z))),i(i(i(x,z),y),y)),i(i(i(x,z),y),y))).
P(i(x,i(y,x))).
P(i(i(i(x,y),x),x)).
P(i(i(x,y),i(i(y,z),i(x,z)))).
end_of_list.
weight_list(pick_and_purge).
% Following is Lukasiewicz's 28 step DS proof sketch (as resonators)
weight(P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(x,i(y,u)))),2).
weight(P(i(i(i(x,i(y,z)),i(i(x,y),i(u,y))),i(v,i(i(x,y),i(u,y))))),2).
weight(P(i(i(i(x,y),x),i(z,x))),2).
weight(P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))),2).
weight(P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))),2).
weight(P(i(i(i(x,i(y,z)),i(u,i(z,v))),i(w,i(u,i(z,v))))),2).
weight(P(i(i(i(x,y),z),i(y,z))),2).
weight(P(i(x,i(i(x,y),i(z,y)))),2).
weight(P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))),2).
weight(P(i(i(i(x,y),i(i(i(y,z),u),i(v,u))),i(w,i(i(i(y,z),u),i(v,u))))),2).
weight(P(i(i(i(x,i(i(i(y,z),u),i(v,u))),i(w,y)),i(v6,i(w,y)))),2).
weight(P(i(i(i(x,i(y,z)),i(u,i(i(i(z,v),w),i(v6,w)))),i(v7,i(u,i(i(i(z,v),w),i(v6,w)))))),2).
weight(P(i(i(i(x,y),i(z,u)),i(i(i(y,v),u),i(z,u)))),2).
weight(P(i(i(i(x,y),i(z,u)),i(i(x,u),i(z,u)))),2).
weight(P(i(i(x,i(y,z)),i(i(i(x,u),z),i(y,z)))),2).
weight(P(i(i(i(i(i(x,y),z),u),i(v,x)),i(i(z,x),i(v,x)))),2).
weight(P(i(i(i(i(x,y),i(z,y)),i(i(i(y,u),x),v)),i(w,i(i(i(y,u),x),v)))),2).
weight(P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,z),u),i(x,y)))),2).
weight(P(i(i(i(i(x,y),y),i(z,y)),i(i(i(y,u),x),i(z,y)))),2).
weight(P(i(i(i(i(x,y),z),z),i(i(z,y),i(x,y)))),2).
weight(P(i(x,x)),2).
weight(P(i(i(i(x,y),z),i(i(z,x),x))),2).
weight(P(i(x,i(i(x,y),y))),2).
weight(P(i(i(x,y),i(i(i(x,z),y),y))),2).
weight(P(i(i(i(i(x,y),i(i(y,z),i(x,z))),i(i(i(x,z),y),y)),i(i(i(x,z),y),y))),2).
weight(P(i(x,i(y,x))),2).
weight(P(i(i(i(x,y),x),x)),2).
weight(P(i(i(x,y),i(i(y,z),i(x,z)))),2).
end_of_list.
list(usable).
% Following is condensed detachment (CD)
-P(i(x,y)) | -P(x) | P(y).
% Following is disjunction of denials of 28 DS proof sketch steps
-P(i(i(i(i(c3,c1),i(c4,c1)),i(c1,c2)),i(c3,i(c1,c2)))) |
-P(i(i(i(c3,i(c1,c2)),i(i(c3,c1),i(c4,c1))),i(c5,i(i(c3,c1),i(c4,c1))))) |
-P(i(i(i(c1,c2),c1),i(c4,c1))) |
-P(i(i(i(c4,c1),i(c1,c2)),i(c3,i(c1,c2)))) |
-P(i(i(i(c3,i(c1,c2)),i(c4,c1)),i(c5,i(c4,c1)))) |
-P(i(i(i(c5,i(c4,c1)),i(c3,i(c1,c2))),i(c6,i(c3,i(c1,c2))))) |
-P(i(i(i(c4,c2),c1),i(c2,c1))) |
-P(i(c3,i(i(c3,c1),i(c4,c1)))) |
-P(i(i(i(i(i(c3,c2),c1),i(c4,c1)),c3),i(c5,c3))) |
-P(i(i(i(c5,c3),i(i(i(c3,c2),c1),i(c4,c1))),i(c6,i(i(i(c3,c2),c1),i(c4,c1))))) |
-P(i(i(i(c6,i(i(i(c3,c2),c1),i(c4,c1))),i(c5,c3)),i(c7,i(c5,c3)))) |
-P(i(i(i(c7,i(c5,c3)),i(c6,i(i(i(c3,c2),c1),i(c4,c1)))),i(c8,i(c6,i(i(i(c3,c2),c1),i(c4,c1)))))) |
-P(i(i(i(c5,c3),i(c4,c1)),i(i(i(c3,c2),c1),i(c4,c1)))) |
-P(i(i(i(c3,c2),i(c4,c1)),i(i(c3,c1),i(c4,c1)))) |
-P(i(i(c3,i(c4,c1)),i(i(i(c3,c2),c1),i(c4,c1)))) |
-P(i(i(i(i(i(c1,c2),c3),c5),i(c4,c1)),i(i(c3,c1),i(c4,c1)))) |
-P(i(i(i(i(c3,c1),i(c4,c1)),i(i(i(c1,c2),c3),c5)),i(c6,i(i(i(c1,c2),c3),c5)))) |
-P(i(i(i(i(c4,c1),c2),i(c3,c1)),i(i(i(c1,c2),c3),i(c4,c1)))) |
-P(i(i(i(i(c3,c1),c1),i(c4,c1)),i(i(i(c1,c2),c3),i(c4,c1)))) |
-P(i(i(i(i(c1,c3),c2),c2),i(i(c2,c3),i(c1,c3)))) |
-P(i(c1,c1)) |
-P(i(i(i(c1,c2),c3),i(i(c3,c1),c1))) |
-P(i(c3,i(i(c3,c1),c1))) |
-P(i(i(c1,c2),i(i(i(c1,c3),c2),c2))) |
-P(i(i(i(i(c1,c2),i(i(c2,c3),i(c1,c3))),i(i(i(c1,c3),c2),c2)),i(i(i(c1,c3),c2),c2))) |
-P(i(c1,i(c2,c1))) |
-P(i(i(i(c1,c2),c1),c1)) |
-P(i(i(c1,c2),i(i(c2,c3),i(c1,c3)))) | $ANS(28_luka_steps).
end_of_list.
list(sos).
% Following is Lukasiewicz's shortest implicational single axiom
P(i(i(i(x,y),z),i(i(z,x),i(u,x)))).
end_of_list.
list(hot).
% Following is condensed detachment (CD)
-P(i(x,y)) | -P(x) | P(y).
% Following is Lukasiewicz's shortest implicational single axiom
P(i(i(i(x,y),z),i(i(z,x),i(u,x)))).
end_of_list.
ukasiewicz's DS Proof Sketch
Length of proof is 36. Level of proof is 29.
---------------- PROOF ----------------
34 [] -P(i(x,y))| -P(x)|P(y).
35 [] -P(i(i(i(i(c3,c1),i(c4,c1)),i(c1,c2)),i(c3,i(c1,c2)))) | ...
36 [] P(i(i(i(x,y),z),i(i(z,x),i(u,x)))).
39 [hyper,34,36,36] P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(v,i(y,u)))).
41 [hyper,34,36,39] P(i(i(i(x,i(y,z)),i(i(u,y),i(v,y))),i(w,i(i(u,y),i(v,y))))).
46 [hyper,34,41,36] P(i(x,i(i(i(y,z),y),i(u,y)))).
47 [hyper,34,46,46] P(i(i(i(x,y),x),i(z,x))).
51 [hyper,34,36,47] P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))).
52 [hyper,34,36,51] P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))).
54 [hyper,34,36,52] P(i(i(i(x,i(y,z)),i(u,i(z,v))),i(w,i(u,i(z,v))))).
57 [hyper,34,54,36] P(i(x,i(i(i(y,z),u),i(z,u)))).
58 [hyper,34,57,57] P(i(i(i(x,y),z),i(y,z))).
60 [hyper,34,58,58] P(i(x,i(y,x))).
62 [hyper,34,58,36] P(i(x,i(i(x,y),i(z,y)))).
81 [hyper,34,36,62] P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))).
93 [hyper,34,36,81] P(i(i(i(x,y),i(i(i(y,z),u),i(v,u))),i(w,i(i(i(y,z),u),i(v,u))))).
98 [hyper,34,36,93] P(i(i(i(x,i(i(i(y,z),u),i(v,u))),i(w,y)),i(v6,i(w,y)))).
101 [hyper,34,36,98] P(i(i(i(x,i(y,z)),i(u,i(i(i(z,v),w),i(v6,w)))),i(v7,i(u,i(i(i(z,v),w),i(v6,w)))))).
106 [hyper,34,101,36] P(i(x,i(i(i(y,z),i(u,v)),i(i(i(z,w),v),i(u,v))))).
107 [hyper,34,106,106] P(i(i(i(x,y),i(z,u)),i(i(i(y,v),u),i(z,u)))).
113 [hyper,34,107,36] P(i(i(i(x,y),i(z,u)),i(i(x,u),i(z,u)))).
117 [hyper,34,113,62] P(i(i(x,i(y,z)),i(i(i(x,u),z),i(y,z)))).
132 [hyper,34,117,36] P(i(i(i(i(i(x,y),z),u),i(v,x)),i(i(z,x),i(v,x)))).
136 [hyper,34,36,132] P(i(i(i(i(x,y),i(z,y)),i(i(i(y,u),x),v)),i(w,i(i(i(y,u),x),v)))).
140 [hyper,34,132,58] P(i(i(x,y),i(x,y))).
143 [hyper,34,136,136] P(i(x,i(i(i(i(y,z),u),i(v,z)),i(i(i(z,w),v),i(y,z))))).
153 [hyper,34,143,143] P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,v),u),i(x,y)))).
158 [hyper,34,107,153] P(i(i(i(i(x,y),z),i(u,y)),i(i(i(y,v),x),i(u,y)))).
172 [hyper,34,158,140] P(i(i(i(x,y),z),i(i(z,x),x))).
175 [hyper,34,158,113] P(i(i(i(i(x,y),z),u),i(i(u,y),i(x,y)))).
185 [hyper,34,58,172] P(i(x,i(i(x,y),y))).
191 [hyper,34,172,140] P(i(i(i(x,y),x),x)).
225 [hyper,34,175,52] P(i(i(i(x,i(y,z)),i(z,u)),i(v,i(z,u)))).
234 [hyper,34,113,185] P(i(i(x,y),i(i(i(x,z),y),y))).
270 [hyper,34,58,191] P(i(x,x)).
276 [hyper,34,36,225] P(i(i(i(x,i(y,z)),i(u,i(v,y))),i(w,i(u,i(v,y))))).
278 [hyper,34,234,234] P(i(i(i(i(x,y),z),i(i(i(x,u),y),y)),i(i(i(x,u),y),y))).
317 [hyper,34,175,278] P(i(i(i(i(i(x,y),z),z),u),i(i(x,z),u))).
337 [hyper,34,317,175] P(i(i(x,y),i(i(y,z),i(x,z)))).
346 [hyper,35,225,...] $ANS(28_luka_steps).
------------ end of proof -------------
References
[1] B. Fitelson and L. Wos.
Finding missing proofs with automated reasoning.
Studia Logica (to appear).
ukasiewicz.
Selected Works.
Noth Holland, 1970.
aw,
1977.
Boolean Algebra and the Sheffer Stroke Problem
Robert Veroff
(veroff@cs.unm.edu)
University of New Mexico
Maria Paola Bonacina
(Secretary of AAR and CADE)
e-mail: bonacina@cs.uiowa.edu
Frank Pfenning, Vice-President (Elected 10/1998)
Harald Ganzinger (Past Program Chair, elected 10/1999)
Claude Kirchner (Past Program Co-chair, elected 10/1998)
William W. McCune (Past Program Chair, elected 8/1997)
David A. Plaisted (Elected 10/1999)
Maria Paola Bonacina (Secretary)
Neil V. Murray (Treasurer)
Tobias Nipkow (IJCAR 2001 Program Co-Chair)
Michael Kohlhase
David McAllester
Andrei Voronkov
Dongming Wang
Mid-conference workshops and excursions will be on July 25-26.
Two conferences
are scheduled in parallel for July 27-30:
Post-conference workshops will be held on
July 31 - August 1. Plenary events involving all the conferences are
planned.
Gail Pieper
2000-08-02