haehnle.ira.uka.de (02/04/91)
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