From: Deepak Kapur <kapur@cs.albany.edu>
Date: Tue, 17 Oct 1995 13:26:48 -0400
Message-Id: <199510171726.NAA01296@sutra.cs.albany.edu>
To: qed@mcs.anl.gov
Subject: abstracts from J. of Automated Reasoning, Vol. 15, No. 3
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


  Titles and abstracts of J. of Automated Reasoning, Vol. 15, No. 3, Dec. 1995


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.