reiner@ira.uka.de (Reiner Haehnle) (03/28/91)
Summary on
T A B L E A U - B A S E D T H E O R E M P R O V I N G
(long)
Some time ago I started a query in this newsgroup for ongoing
activities in tableau-based automated theorem proving, and/or
many-valued logics. Since I received a surprisingly high number of
responses I thought there might be enough interest to justify a
summary.
Some informations occurred in several mails and I chose to
remove duplicates in this summary, so perhaps not all people who
sent me informations are actually mentioned. On the other hand I
decided to include also a few references brought to me from
other sources that seemed appropriate. My thanks, however, go
to all contributors.
The summary is structured as follows:
I) PAPERS and BOOKS
a) General
b) Special Topics
II) PROJECTS and PEOPLE
III) SYSTEMS
Here we go -
I) PAPERS and BOOKS
a) General - Many people mentioned the following books and papers on
tableaux:
The standard reference:
@BOOK{Smullyan68,
author = {Raymond Smullyan},
title = {First-Order Logic},
publisher = {Springer, New York},
year = {1968},
edition = {second},
keywords = {semantic tableaux, proof theory, completeness, interpolation, logic} }
__
A more recent publication, excellently written. It covers also
resolution and other methods and contains a prolog implementation of a
tableau-based theorem prover:
@BOOK{Fitting90d,
author = {Melvin C. Fitting},
title = {First-Order Logic and Automated Theorem Proving},
publisher = {Springer, New York},
year = {1990},
keywords = {first-order logic, automated theorem proving, semantic tableaux} }
__
The description of an efficient tableau-based prover written in LISP
is contained in:
@Article{OppacherSuen88,
author = {F. Oppacher and E. Suen},
title = {{HARP}: A Tableau-Based Theorem Prover},
journal = {Journal of Automated Reasoning},
year = {1988},
volume = {4},
pages = {69 -- 100},
keywords = {semantic tableau, automated theorem proving} }
__
b) Special Topics:
Bob Riemenschneider <rar@ads.com> recommends the following paper:
@InBook{Bowen82,
author = {K.A. Bowen},
title = {Programming with full first-order logic},
publisher = {Ellis Horwood, Chichester},
year = {1982},
pages = {421--440},
volume = {10},
series = {Machine Intelligence},
keywords = {sequent calculus, automated deduction} }
__
Tableau Methods for modal and inituitionistic logics may be found in:
@BOOK{Fitting83,
author = {Melvin C. Fitting},
title = {Proof Methods for Modal and Intutionistic Logics},
publisher = {Reidel, Dordrecht},
year = {1983},
keywords = {modal logic, intuitionistic logic, semantic tableaux,
proof theory, interpolation, completeness} }
And, with a focus on automated deduction, in:
@BOOK{Wallen90,
author = {Lincoln A. Wallen},
title = {Automated Proof Search in Non-Classical Logics},
publisher = {{MIT} {P}ress},
year = {1990},
keywords = {modal logic, intuitionistic logic, matrix method,
sequent calculus, semantic tableaux} }
__
On adding equality to tableaux:
@Article{Reeves87,
author = {S. V. Reeves},
title = {Adding Equality to Semantic Tableaux},
journal = {Journal of Automated Reasoning},
year = {1987},
volume = {3},
pages = {225 -- 246},
keywords = {equality, semantic tableaux, automated theorem proving} }
__
II) PROJECTS and PEOPLE
Mark Grundy <Mark.Grundy@arp.anu.edu.au> (Australian Reasoning
Project) writes:
... Presently, I'm working on defining a relationship between
resolution and tableau proof methods. During my doctoral work, I
developed a condensed, tableau-like system (called ``cameo''),
which seems to speed up tableau-style proofs quite markedly. ...
and provided also the following papers:
@Article{Grundy91a,
author = {Mark Grundy},
title = {Cameo: Refutation Proving by Unordered Model Classifications},
journal = {To appear in Journal of Automated Reasoning},
year = {1991},
keywords = {semantic tableaux, automated theorem proving, resolution} }
@TechReport{Grundy91b,
author = {Mark Grundy},
title = {Correctness of Resolution Methods for Determining {C}ameo
Theoremhood and Tableau Closure},
institution = {Automated Reasoning Project, Australian National University},
year = {1991},
address = {markg@arp.anu.oz.au},
month = {January},
keywords = {semantic tableaux, resolution} }
__
Also from ARP, Jacques Riche <Jacques.Riche@arp.anu.edu.au> writes:
... The person to contact here about tableau provers is Rod Girle
rag@arp.anu.edu.au
Also John Slaney, who is an expert on x-valued logics and many
other topics.
About tableaux and modal logic, Luis Farinas at
farinas@irit.fr
who could tell you more about people working in this field in
France. ...
__
Ian Gent <ipg@cs.warwick.ac.uk> writes:
I am very interested in tableaux based theorem proving, and indeed
there seems to be a fair community in Britain who are. For instance,
if you contact Krysia Broda and Richard Cunningham at Imperial
College London...
... Some very nice work has been done by Marcello D'Agostino on the
tableaux-like proof systems KE and KI, showing their relationship
with tableaux. He has also produced a tableaux system for Andeerson
and Belnap's Relevant Entailment. His PhD thesis (1990) is available
from the Programming Research Group in Oxford, as Technical Monograph
number 88 ...
__
Robert Johnson <robj@cs.qmw.ac.uk> writes:
I have been sent a copy of your mail message regarding tableaux
research since I'm one of the few with an ongoing interest in
them. I'm doing research into parallelising the approach and
shall be using Strand for that purpose. I also believe that
Melvyn Fitting at CUNY has some similar research about to
commence using C-Linda on a number of Suns.
__
Graham Wrightson <graham@nucs.newcastle.edu.au> (currently Technical
University Munich) has been interested in Tableaux for some years. His
current research interest includes the relationship between Tableaux and
Clause Graph Resolution.
A former paper by Wrightson is:
@TechReport{Wrightson84a,
author = {Graham Wrightson},
title = {Semantic Tableaux, Unification and Links},
institution = {Victoria University of Wellington},
year = {1984},
number = {CSD--ANZARP--84--001},
keywords = {connection graph,indexing,semantic tableaux,automated theorem proving} }
__
Eric Rosenthal and Neil Murray have devised a rule called
'dissolution' that can speed up tableau proofs considerable:
@TechReport{MurrayRosenthal90a,
author = {Neil V. Murray and Erik Rosenthal},
title = {On the relative merits of path dissolution and the method of
analytical tableaux},
institution = {Dept. of Computer Science, University of Albany},
year = {1990},
number = {TR 90-5},
keywords = {dissolution, resolution, matrix method, semantic tableaux,
automated theorem proving} }
They have also a theorem prover based on this rule.
__
Peter A. Flach <flach@kub.nl> writes:
At the Dept. of Philosophy at Tilburg University, there is a research
project called 'improving TABLOG'. The people involved are prof.
Harry de Swart and Willy Ophelders. I don't think they have an
Internet connection, but they can be reached at the following
address:
Dept. of Philosophy
Tilburg University
POBox 90153
5000 LE Tilburg
the Netherlands
+31 13 66 2415/3018/2985
__
III) SYSTEMS:
VS Subrahmanian <vs@cs.umd.edu> writes:
Jim Lu, Larry Henschen, myself and Newton da Costa have
an implementation of a theorem prover for certain kinds of
many valued logics. These are NOT tableau based, but
rather are based on some resolution-like strategies
developed by us. There is a paper on this in
CADE-90, and a later, more detailed version that will
appear in the "Festschrift for Woody Bledsoe" edited
by Bob Boyer.
__
Chet Murthy <murthy@cs.cornell.edu> writes:
The Nuprl system is a tableaux-based system also. ...
... There is the work of Harper (Robert Harper's thesis) in
which he does some stuff regarding the "constructible subgoals"
property of the Nuprl logic. There has been little written about the
actual design methodology of the logic, though. ...
__
Shinji Kono <kono%csl.sony.jp@relay.cs.net> writes:
I have a tableau-based verifier for propositional linear time
temporal logic. This is pretty popular, I think...
and provided the following references:
@inproceedings{vlsi87,
author = "H. Nakamura and M. Fujita and S. Kono",
title = "Temporal Logic Based Fast Verification System Using Cover Expressions",
booktitle = "VLSI '87",
year = 1987}
@INPROCEEDINGS{fujita83,
AUTHOR = "M. Fujita",
TITLE = "Verification with Prolog and Temporal Logic",
BOOKTITLE = "CHDL '83",
ORGANIZATION = "IFIP",
YEAR = 1983}
@INPROCEEDINGS{fujita85,
AUTHOR = "M. Fujita",
TITLE = "Logic Design Assistance with Temporal Logic",
BOOKTITLE = "CHDL '85",
ORGANIZATION = "IFIP",
PAGES = "129-138",
YEAR = 1985}
@TECHREPORT{wolper82,
AUTHOR = "P. Wolper",
TITLE = "Synthesis of Communicating Processes from
Temporal Logic Specifications",
INSTITUTION = "Stanford University",
NUMBER = "STAN-CS-82-925",
YEAR = 1982}
__
Fujita Masayuki <mfujita%icot.or.jp@relay.cs.net>, ICOT, Tokyo writes:
... We are involved in the parallel prover project
which was launched beggining of last year. We are concerned with
theorem prover and program synthesis as its application.
We are developping parallel theorem prover on the paralell inference
macnine:PIM. The basic function of it is alike tableau method. ...
Dr. Fujita provided also several papers on this project for me:
@TechReport{FHSK91,
author = {Masayuki Fujita and Ryuzo Hasegawa and Yasayuki Shirai and Fumihiro Kumeno},
title = {Program Synthesis by a Model Generation Theorem Prover},
institution = {Institute for New Generation Computer Technology, Tokyo},
year = {1991},
month = {February},
keywords = {model generation, automated theorem proving, program synthesis} }
@TechReport{FujitaHasegawa91,
author = {Hiroshi Fujita and Ryuzo Hasegawa },
title = {A Model Generation Theorem Prover in {KL1} Using a Ramified-Stack Algorithm},
institution = {Institute for New Generation Computer Technology, Tokyo},
year = {1991},
number = {TR--606},
annote = {Also in Proc. of ICLP 91},
keywords = {model generation, automated theorem proving, program synthesis} }
@TechReport{HFF90,
author = {Ryuzo Hasegawa and Hiroshi Fujita and Masayuki Fujita},
title = {A Parallel Theorem Prover in {KL1} and its Application to Program Synthesis},
institution = {Institute for New Generation Computer Technology, Tokyo},
year = {1990},
number = {TR--588},
keywords = {model generation, automated theorem proving, program synthesis} }
__
Sakai Ko <sakai%icot.or.jp@relay.cs.net>, ICOT, Tokyo writes:
I have prototype tableau based provers for classical FOL (first order
logic), intuitionistic PL (propositional logic) and modal PL for
systems T, S4, S5. The PL provers works fast enough. I confess the
FOL prover is not satisfactory, but I believe that it will get much
faster, if a good strategy is employed. Unfortunately, I do not have
time to study such a strategy. If you are interested, I will send
the program to you. The program is written in Sicstus Prolog, but
runs on every standard Prolog system (for example, Quintus).
Dr. Sakai was also friendly enough to give me his program. I have
tested it successfully on Quintus Prolog 2.4 and 3.0.
__
Wolfgang Schoenfeld, Peter Schmitt and Wolfgang Wernecke at the Institute for
Knowledge-Based Systems at IBM in Heidelberg, Germany have been
developing tableau-based theorem provers for first-order logic with
various extensions for some years. The latest system is implemented
in Quintus Prolog.
@TechReport{Schmitt87a,
author = {Peter H. Schmitt},
title = {The {THOT} Theorem Prover},
institution = {IBM Heidelberg Scientific Center},
year = {1987},
number = {TR--87.09.007},
keywords = {automated theorem proving, semantic tableaux, THOT} }
@TechReport{SchmittWernecke90,
author = {Peter H. Schmitt and Wolfgang Wernecke},
title = {Tableau Calculus for Order Sorted Logic},
institution = {{IWBS}, IBM Deutschland},
year = {1990},
number = {{IWBS} Report 108},
month = {January},
keywords = {semantic tableaux, order sorted logic, automated theorem proving} }
@InProceedings{Schoenfeld85,
author = {Wolfgang Sch\"{o}nfeld},
title = {{PROLOG} Extensions based on Tableau Calculus},
booktitle = {Proceedings {IJCAI} 85},
year = {1985},
pages = {730 -- 732},
keywords = {semantic tableau, automated theorem proving, prolog} }
__
Thomas Kaeufl <kaeufl@ira.uka.de> has written a tableau-based theorem
prover as part of a system for program verification, implemented in
LISP.
Nicolas Zabel <zabel@nereide.imag.fr> added equality to this system
and has also written a tableau-based prover for many-valued logics
based on the work of Carnielli:
@Article{CaferraZabel90,
author = {Ricardo Caferra and Nicolas Zabel},
title = {An application of many-valued logic to decide propositional $S_{5}$
formulae: a strategy designed for a parameterized
tableaux-based theorem prover},
journal = {Artificial Intelligence IV:Methodology, Systems, Applications},
year = {1990},
pages = {23 -- 32},
keywords = {multiple-valued logic, semantic tableaux, automated theorem proving,
modal logics} }
@Article{Carnielli87,
author = {Walter A. Carnielli},
title = {Systematization of Finite Many-Valued Logics through the Method of Tableaux},
journal = {Journal of Symbolic Logic},
year = {1987},
volume = {52},
number = {2},
pages = {473--493},
month = {June},
keywords = {semantic tableaux, proof theory, multiple-valued logics} }
__
End of Summary.
Thank you very much again, all who contributed to this list.
--
( Reiner H"ahnle Phone: ++49-721-608-4329 )
) Institute for Logic, Complexity Fax: ++49-721-69 77 60 (
( and Deduction Systems e-mail: haehnle@ira.uka.de )
) University of Karlsruhe (
( Am Fasanengarten 5 'Nichts, Niemand, Nirgends, Nie, )
) 7500 Karlsruhe Nichts, Niemand, Nirgends, Nie' (
( Fed. Rep. of Germany -- Arno Schmidt )