Embedding negation as failure into a model generation theorem prover

Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa

Research output: Chapter in Book/Report/Conference proceedingConference contribution

46 Citations (Scopus)

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 languageEnglish
Title of host publicationAutomated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings
EditorsDeepak Kapur
PublisherSpringer Verlag
Pages400-415
Number of pages16
ISBN (Print)9783540556022
Publication statusPublished - Jan 1 1992
Event11th International Conference on Automated Deduction, CADE, 1992 - Saratoga Springs, United States
Duration: Jun 15 1992Jun 18 1992

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume607 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other11th International Conference on Automated Deduction, CADE, 1992
CountryUnited States
CitySaratoga Springs
Period6/15/926/18/92

Fingerprint

Negation as Failure
Answer Sets
Deductive Databases
Integrity Constraints
Fixpoint
Minimal Model
Bottom-up
Logic Programs
Theorem
Reasoning
Unstable
Model
Beliefs
Class

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Inoue, K., Koshimura, M., & Hasegawa, R. (1992). Embedding negation as failure into a model generation theorem prover. In D. Kapur (Ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings (pp. 400-415). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI). Springer Verlag.

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 proceedingConference contribution

Inoue, K, Koshimura, M & Hasegawa, R 1992, Embedding negation as failure into a model generation theorem prover. in D Kapur (ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 607 LNAI, Springer Verlag, pp. 400-415, 11th International Conference on Automated Deduction, CADE, 1992, Saratoga Springs, United States, 6/15/92.
Inoue K, Koshimura M, Hasegawa R. Embedding negation as failure into a model generation theorem prover. In Kapur D, editor, Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1992. p. 400-415. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Inoue, Katsumi ; Koshimura, Miyuki ; Hasegawa, Ryuzo. / Embedding negation as failure into a model generation theorem prover. Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. editor / Deepak Kapur. Springer Verlag, 1992. pp. 400-415 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{ba4e5b35a3dc4ab0a1700590369cc59a,
title = "Embedding negation as failure into a model generation theorem prover",
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.",
author = "Katsumi Inoue and Miyuki Koshimura and Ryuzo Hasegawa",
year = "1992",
month = "1",
day = "1",
language = "English",
isbn = "9783540556022",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "400--415",
editor = "Deepak Kapur",
booktitle = "Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings",
address = "Germany",

}

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 -