Z-Resolution: Theorem-Proving with Compiled Axioms

Publisher Website
Google Scholar
Abstract
An improved procedure for resolution theorem proving, called Z-resolution, is described. The basic idea of Z-resolution is to “compile” some of the axioms in a deductive problem. This means to automatically transform the selected axioms into a computer program which carries out the inference rules indicated by the axioms. This is done automatically by another program called the specializer. The advantage of doing this is that the compiled axioms run faster, just as a compiled program runs faster than an interpreted program. A proof is given that the inference rule used in Z-resolution is complete, provided that the axioms “compiled” have certain properties.

This publication has 7 references indexed in Scilit: