Access Restriction

Author Dixon, John K.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1973
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1973-01-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 20
Issue Number 1
Page Count 21
Starting Page 127
Ending Page 147

Open content in new tab

   Open content in new tab
Source: ACM Digital Library