Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

9

TABLEAUX
1997
Springer

favoriteEmaildiscussreport

98views Artificial Intelligence» more TABLEAUX 1997»

ileanTAP: An Intuitionistic Theorem Prover

13 years 8 months ago

ileanTAP: An Intuitionistic Theorem Prover

Download www.jens-otten.de

We present a Prolog program that implements a sound and complete theorem prover for ﬁrst-order intuitionistic logic. It is based on free-variable semantic tableaux extended by an additional string uniﬁcation to ensure the particular restrictions in intuitionistic logic. Due to the modular treatment of the diﬀerent logical connectives the implementation can easily be adapted to deal with other non-classical logics.

Jens Otten

Real-time Traffic

Artificial Intelligence | Complete Theorem Prover | Intuitionistic Logic | TABLEAUX 1997 | ﬁrst-order Intuitionistic Logic |

claim paper

Related Content

» The ILTP Library Benchmarking Automated Theorem Provers for Intuitionistic Logic

» Clausal ConnectionBased Theorem Proving in Intuitionistic FirstOrder Logic

» STRIP Structural Sharing for Efficient ProofSearch

» A Focusing Inverse Method Theorem Prover for FirstOrder Linear Logic

» Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

» Proof Terms for Simply Typed Higher Order Logic

» Deciding Intuitionistic Propositional Logic via Translation into Classical Logic

» JProver Integrating ConnectionBased Theorem Proving into Interactive Proof Assistants

» Using the Temporal Logic RDL for Design Specifications

Post Info
More Details (n/a)

Added	08 Aug 2010
Updated	08 Aug 2010
Type	Conference
Year	1997
Where	TABLEAUX
Authors	Jens Otten

Comments (0)