Thumbnail
Access Restriction
Subscribed

Author Chang, C. L.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1970
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract A resolution in which one of the two parent clauses is a unit clause is called a unit resolution, whereas a resolution in which one of the two parent clauses is an original input clause is called an input resolution. A unit (input) proof is a deduction of the empty clause □ such that every resolution in the deduction is a unit (input) resolution. It is proved in the paper that a set $\textit{S}$ of clauses containing its unit factors has a unit proof if and only if $\textit{S}$ has an input proof. A LISP program implementing unit resolution is described and results of experiments are given.
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 1970-10-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 17
Issue Number 4
Page Count 10
Starting Page 698
Ending Page 707


Open content in new tab

   Open content in new tab
Source: ACM Digital Library