ileanTAP: An intuitionistic theorem prover
| Author(s) : | Technische Hochschule Darmstadt Fachbereich Informatik Fachbereich Informatik Fachgebiet Intellektik Fachgebiet Intellektik Jens Otten Jens Otten Technische Hochschule Darmstadt, |
| Publisher : | N/A |
| Publication Date : | 1997 |
| ISSN : | N/A |
| Abstract : | Abstract. We present a Prolog program that implements a sound and complete theorem prover for first-order intuitionistic logic. It is based on free-variable semantic tableaux extended by an additional string unification to ensure the particular restrictions in intuitionistic logic. Due to the modular treatment of the different logical connectives the implementation can easily be adapted to deal with other non-classical logics. 1, |