The hyper tableaux calculus with equality and an application to finite model computation. (English) Zbl 1193.03025
The authors show how to incorporate efficient ordering-based equality inference rules and redundancy elimination techniques into a tableau calculus. This approach is based on splitting of positive clauses and an adapted version of the superposition inference rules.
The soundness and completeness of the calculus are proved. This calculus is a non-trivial decision procedure for function-free clause logic with equality, which captures the complexity class NEXPTIME.
The soundness and completeness of the calculus are proved. This calculus is a non-trivial decision procedure for function-free clause logic with equality, which captures the complexity class NEXPTIME.
Reviewer: Nail Zamov (Kazan)
MSC:
03B35 | Mechanization of proofs and logical operations |
68Q15 | Complexity classes (hierarchies, relations among complexity classes, etc.) |
68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |