Abstract
Here, for the first time, we give an implementation which computes answer sets of every class of (function-free) logic programs and deductive databases containing both negation as failure and classical negation. The proposal is based on bottom-up, incremental, backtrack-free computation of the minimal models of positive disjunctive programs, together with integrity constraints over beliefs and disbeliefs. Our translation method not only provides a simple fixpoint characterization of answer sets, but also is very helpful to understand under what conditions each model is “stable” or “unstable”. The procedure has been implemented on top of the model generation theorem prover MGTP on a parallel inference machine, and has been applied to a legal reasoning system.
| Original language | English |
|---|---|
| Title of host publication | Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings |
| Editors | Deepak Kapur |
| Publisher | Springer Verlag |
| Pages | 400-415 |
| Number of pages | 16 |
| ISBN (Print) | 9783540556022 |
| Publication status | Published - Jan 1 1992 |
| Event | 11th International Conference on Automated Deduction, CADE, 1992 - Saratoga Springs, United States Duration: Jun 15 1992 → Jun 18 1992 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 607 LNAI |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 11th International Conference on Automated Deduction, CADE, 1992 |
|---|---|
| Country | United States |
| City | Saratoga Springs |
| Period | 6/15/92 → 6/18/92 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Computer Science(all)
Cite this
Embedding negation as failure into a model generation theorem prover. / Inoue, Katsumi; Koshimura, Miyuki; Hasegawa, Ryuzo.
Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. ed. / Deepak Kapur. Springer Verlag, 1992. p. 400-415 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Embedding negation as failure into a model generation theorem prover
AU - Inoue, Katsumi
AU - Koshimura, Miyuki
AU - Hasegawa, Ryuzo
PY - 1992/1/1
Y1 - 1992/1/1
N2 - Here, for the first time, we give an implementation which computes answer sets of every class of (function-free) logic programs and deductive databases containing both negation as failure and classical negation. The proposal is based on bottom-up, incremental, backtrack-free computation of the minimal models of positive disjunctive programs, together with integrity constraints over beliefs and disbeliefs. Our translation method not only provides a simple fixpoint characterization of answer sets, but also is very helpful to understand under what conditions each model is “stable” or “unstable”. The procedure has been implemented on top of the model generation theorem prover MGTP on a parallel inference machine, and has been applied to a legal reasoning system.
AB - Here, for the first time, we give an implementation which computes answer sets of every class of (function-free) logic programs and deductive databases containing both negation as failure and classical negation. The proposal is based on bottom-up, incremental, backtrack-free computation of the minimal models of positive disjunctive programs, together with integrity constraints over beliefs and disbeliefs. Our translation method not only provides a simple fixpoint characterization of answer sets, but also is very helpful to understand under what conditions each model is “stable” or “unstable”. The procedure has been implemented on top of the model generation theorem prover MGTP on a parallel inference machine, and has been applied to a legal reasoning system.
UR - http://www.scopus.com/inward/record.url?scp=84959408863&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84959408863&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84959408863
SN - 9783540556022
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 400
EP - 415
BT - Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings
A2 - Kapur, Deepak
PB - Springer Verlag
ER -