A superposition oriented theorem prover

AbstractThis paper describes a theorem proving procedure which combines the approach of Resolution with that of Rewriting. The basic-theoretical result is the completeness of a strong restriction of paramodulation for locking resolution procedures. Its oriented character suggests to consider the restricted paramodulation as a form of superposition (the Rewriting operation). This is achieved by means of a new formalism of clauses, named equational clauses, in which each literal is converted into an equation. Thereby, superposition on equational clauses is shown to embody not only paramodulation but also binary resolution; so clausal superposition will build up our major rule of inference. In addition, term simplification is incorporated in our procedure as well as subsumption. Experimental results and potential applications for our theorem prover are lastly reported