Completeness of hyper-resolution via the semantics of disjunctive logic programs |
| |
| Authors: | Linh Anh Nguyen,Rajeev Goré |
| |
| Affiliation: | a Institute of Informatics, University of Warsaw, ul. Banacha 2, 02-097 Warsaw, Poland
b RSISE and NICTA, The Australian National University, Canberra ACT 0200, Australia |
| |
| Abstract: | We present a proof of completeness of hyper-resolution based on the fixpoint semantics of disjunctive logic programs. This shows that hyper-resolution can be studied from the point of view of logic programming. |
| |
| Keywords: | Fixpoint semantics Automatic theorem proving |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
