SEARCHING FOR CIRCLES OF PURE PROOFS
by Larry Wos
When given a set of properties or conditions (say, three) that are
claimed to be equivalent, the claim can be verified by supplying what
we call a {\it circle of proofs.} In the case in point, one proves
the second property or condition from the first, the third from
the second, and the first from the third. If the proof that 1
implies 2 does not rely on 3, then we say that the proof is pure
with respect to 3, or simply say the {\it proof is pure.}
If one can renumber the three properties or conditions in such a way
that one can find a circle of three pure proofs---technically, each
proof pure with respect to the condition that is neither the
hypothesis nor the conclusion---then we say that a {\it circle of
pure proofs} has been found. Here we study the specific question
of the existence of a circle of pure proofs for the thirteen shortest
single axioms for equivalential calculus, subject to the requirement
that condensed detachment be used as the rule of inference.
For an indication of the difficulty of answering the question, we note
that a single application of condensed detachment to the (shortest single)
axiom known as $P4$ (also known as $UM$) with itself yields the
(shortest single) axiom $P5$ (also known as $XGF$), and two
applications of condensed detachment beginning with $P5$ as hypothesis
yields $P4$. Therefore, except for $P5$, one cannot find a pure
proof of any of the twelve shortest single axioms when using $P4$
as hypothesis or axiom, for the first application of condensed
detachment must focus on two copies of $P4$, which results in the
deduction of $P5$, forcing $P5$ to be present in all proofs that use
$P4$ as the only axiom. Further, the close proximity in the proof
sense of $P4$ when using as the only axiom $P5$ threatens to make
impossible the discovery of a circle of pure proofs for the entire
set of thirteen shortest single axioms. Perhaps more important than
our study of pure proofs, and of a more general nature, we also
present the methodology used to answer the cited specific question,
a methodology that relies on various strategies and features
offered by W. McCune's automated reasoning program \otter\.
The strategies and features of \otter\ we discuss here offer
researchers the needed power to answer deep questions and solve
difficult problems. We close this article (in the last two sections)
with some challenges and some topics for research and (in the
Appendix) with a sample input file and some proofs for study.
A SET-THEORETIC TRANSLATION METHOD FOR POLYMODAL LOGICS
by G. D'Agostino, A. Montanari and A. Policriti
ABSTRACT: The paper presents a {\it set-theoretic translation
method} for polymodal logics that reduces derivability in a
large class of propositional polymodal logics to derivability
in a very weak first-order set theory \Omega. Unlike most existing
translation methods, the one we propose applies to any normal
complete finitely axiomatizable polymodal logic, regardless
of whether it is first-order complete or an explicit semantics
is available. The finite axiomatizability of \Omega allows one
to implement mechanical proof-search procedures via the deduction
theorem. Alternatively, more specialized and efficient techniques
can be employed. In the last part of the paper, we briefly
discuss the application of {\it set T-resolution} to support
automated derivability in (a suitable extension of) \Omega.
lean {\it T$^A$P}: LEAN TABLEAU-BASED DEDUCTION
by Bernhard Beckert and Joachim Posegga
ABSTRACT:
"prove((E,F),A,B,C,D) :- !, prove(E,[F|A],B,C,D).
prove((E;F),A,B,C,D) :- !, prove(E,A,B,C,D), prove(F,A,B,C,D).
prove(all(H,I),A,B,C,D) :- !,
\+ length(C,D), copy_term((H,I,C),(G,F,C)),
append(A,[all(H,I)],E), prove(F,E,B,[G|C],D).
prove(A,_,[C|D],_,_) :-
((A= -(B); -(A)=B)) -> (unify(B,C); prove(A,[],D,_,_)).
prove(A,[E|F],B,C,D) :- prove(E,F,[A|B],C,D)."
implements a first-order theorem-prover based on free-variable
semantic tableaux. It is complete, sound, and efficient.
BRANCHING RULES FOR SATISFIABILITY
by J.N. Hooker and V. Vinay
ABSTRACT: Recent experience suggests that branching algorithms are
among the most attractive for solving propositional satisfiability
problems. A key factor in their success is the rule they use to
decide on which variable to branch next. We attempt to explain and
improve the performance of branching rules with an empirical
model-building approach. One model is based on the rationale given
for the Jeroslow-Wang rule, variations of which have performed
well in recent work. The model is refuted by carefully designed
computational experiments. A second model explains the success of
the Jeroslow-Wang rule, makes other predictions confirmed by
experiment, and leads to the design of branching rules that are
clearly superior to Jeroslow-Wang.