An Automated Theorem Prover Based on Connection Tableau Calculi with Disjunctive Constraints.

Ortrun Ibens Marc Fuchs

Published in: Int. J. Artif. Intell. Tools (2001)

Keyphrases

theorem prover
automated theorem proving
disjunctive constraints
proof search
theorem proving
first order logic
inference rules
reducing the search space
term rewriting
computer algebra
formal proof
boolean algebra
natural deduction
description logics
proof planning
constraint satisfaction problems
domain specific