Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!mcsun!unido!ira.uka.de!news
From: haehnle.ira.uka.de
Newsgroups: comp.theory
Subject: Tableau-Based Theorem Proving
Keywords: ATP, semantic tableaux
Message-ID: <91.035.10:36:07@ira.uka.de>
Date: 4 Feb 91 10:36:07 GMT
Sender: news@ira.uka.de (USENET News System)
Organization: University of Karlsruhe
Lines: 36

Hello everybody,

this is a query for ongoing activities in the development and
application of tableau-based theorem provers.

Our group is currently developing a tableau-based theorem prover suitable
for standard and many-valued first-order logic. Although tableau
techniques are often used in theoretical investigations and, for
pedagogical reasons, in introductory texts, there is few literature on
this topic. The reason is probably that tableau techniques are
usually considered to be less efficient than resolution. 

We believe, however, that it is well worth to investigate tableau techniques
further than it has been done so far, especially if one is interested e.g.
in natural problem representation or non-standard logics.

We would like to know if there are any ongoing activities or projects
that are concerned with tableau-based theorem proving and we invite you
to share experiences, references etc. in this area of research with us.

We would also like to hear about many-valued theorem provers, even if they
are not tableau-based.

Please answer by e-mail to the address given below.

Thank you very much.

Reiner Haehnle
Institute for Logic, Complexity and Deduction Systems
University of Karlsruhe
Kaiserstr. 12
7500 Karlsruhe
FRG

Phone: (0)721-608-4329
email: haehnle@ira.uka.de