ISSN:
1573-0670
Keywords:
automated theorem proving
;
competition
;
RRTP
;
replacement
;
instance based theorem prover
;
propositional calculus decision procedure
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract The Replacement Rule Theorem Prover (RRTP) is an instance-based, refutational, first-order clausal theorem prover. The prover is motivated by the idea of selectively replacing predicates by their definitions, and operates by selecting relevant instances of the input clauses. The relevant instances are grounded, if necessary, and tested for unsatisfiability by using a fast propositional calculus decision procedure.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1005847700447
Permalink