A Prolog-based Proof Tool for Type-Theory TA-lambda and Implicational Intuitionistic-Logic.

L. Yohanes Stefanus Ario Santoso

Published in: IWIL@LPAR (2010)

Keyphrases

intuitionistic logic
proof theoretic
linear logic
proof theory
natural deduction
constraint logic programming
theorem proving
logic programming
knowledge representation
theorem prover
nonmonotonic reasoning
knowledge base
default reasoning
automated reasoning
high level
sequent calculus
relational databases