Proof Procedures and Axiom Sets in Petri Net Models of Horn Clause Propositional Logic--Minimum Modification for Provability--

Toshimasa WATANABE; Naomoto KATO; Kenji ONAGA

Proof Procedures and Axiom Sets in Petri Net Models of Horn Clause Propositional Logic--Minimum Modification for Provability--

Toshimasa WATANABE, Naomoto KATO, Kenji ONAGA

Full Text Views

0

Cite this

Summary :

The subject of the paper is to analyze time complexity of the minimum modification problem in the Horn clause propositional logic. Given a set H of Horn clauses and a query Q in propositional logic, we say that Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens among clauses of H. Suppose that Q is not provable over H, and we are going to modify H and Q into H and Q , respectively, such that Q is provable over H . The problem of making such modification by minimum variable deletion (MVD), by minimum clause addition (MCA) or by their combination (MVDCA) is considered. Each problem is shown to be NP-complete, and some approximation algorithms with their experimental evaluation are given.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E75-A No.4 pp.478-491

Publication Date: 1992/04/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Issue on Discrete Mathematics and Its Application)

Category

Cite this

Copy

Toshimasa WATANABE, Naomoto KATO, Kenji ONAGA, "Proof Procedures and Axiom Sets in Petri Net Models of Horn Clause Propositional Logic--Minimum Modification for Provability--" in IEICE TRANSACTIONS on Fundamentals, vol. E75-A, no. 4, pp. 478-491, April 1992, doi: .
Abstract: The subject of the paper is to analyze time complexity of the minimum modification problem in the Horn clause propositional logic. Given a set H of Horn clauses and a query Q in propositional logic, we say that Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens among clauses of H. Suppose that Q is not provable over H, and we are going to modify H and Q into H and Q , respectively, such that Q is provable over H . The problem of making such modification by minimum variable deletion (MVD), by minimum clause addition (MCA) or by their combination (MVDCA) is considered. Each problem is shown to be NP-complete, and some approximation algorithms with their experimental evaluation are given.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e75-a_4_478/_p

Copy

@ARTICLE{e75-a_4_478,
author={Toshimasa WATANABE, Naomoto KATO, Kenji ONAGA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Proof Procedures and Axiom Sets in Petri Net Models of Horn Clause Propositional Logic--Minimum Modification for Provability--},
year={1992},
volume={E75-A},
number={4},
pages={478-491},
abstract={The subject of the paper is to analyze time complexity of the minimum modification problem in the Horn clause propositional logic. Given a set H of Horn clauses and a query Q in propositional logic, we say that Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens among clauses of H. Suppose that Q is not provable over H, and we are going to modify H and Q into H and Q , respectively, such that Q is provable over H . The problem of making such modification by minimum variable deletion (MVD), by minimum clause addition (MCA) or by their combination (MVDCA) is considered. Each problem is shown to be NP-complete, and some approximation algorithms with their experimental evaluation are given.},
keywords={},
doi={},
ISSN={},
month={April},}

Copy

TY - JOUR
TI - Proof Procedures and Axiom Sets in Petri Net Models of Horn Clause Propositional Logic--Minimum Modification for Provability--
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 478
EP - 491
AU - Toshimasa WATANABE
AU - Naomoto KATO
AU - Kenji ONAGA
PY - 1992
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E75-A
IS - 4
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - April 1992
AB - The subject of the paper is to analyze time complexity of the minimum modification problem in the Horn clause propositional logic. Given a set H of Horn clauses and a query Q in propositional logic, we say that Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens among clauses of H. Suppose that Q is not provable over H, and we are going to modify H and Q into H and Q , respectively, such that Q is provable over H . The problem of making such modification by minimum variable deletion (MVD), by minimum clause addition (MCA) or by their combination (MVDCA) is considered. Each problem is shown to be NP-complete, and some approximation algorithms with their experimental evaluation are given.
ER -