The Satisfiability Problems for Some Classes of Extended Horn Sets in the Propositional Logic

Susumu YAMASAKI; Shuji DOSHITA

The Satisfiability Problems for Some Classes of Extended Horn Sets in the Propositional Logic

Susumu YAMASAKI, Shuji DOSHITA

Full Text Views

0

Cite this

Summary :

The Horn set is the set of Horn clauses. The Horn clause is the set of literals which contains at most one positive literal, where a positive literal means a literal without negation sign. The satisfiability problem of the Horn set in propositional logic is one of P-complete problems, although the satisfiability problem of the formula in propositional logic is one of typical NP-complete problems. In propositional logic, unit and input resolutions, proposed by C. L. Chang, are complete inference rules used to detect the satisfiability of the Horn set. In this paper, we formulate a Restricted Linear (RL) deduction, extending unit and input resolutions. The RL deduction is formed by layering linear deductions each of which corresponds to an input resolution refutation, and is called by another name, a Linear Layered Resolution deduction based on Input resolution (an LLRI deduction). Next, we formulate a Nonlinear Layered Resolution deduction based on Input resolutions (an NLRI deduction). By means of the LLRI and NLRI deductions, we propose some classes of extended Horn sets in propositional logic for which the satisfiability problems are solvable by LLRI and NLRI deductions in deterministic polynomial time; and, thus, so are P-complete. Also we propose algorithms to determine whether a given set of clauses is in the proposed classes of extended Horn sets.

Publication: IEICE TRANSACTIONS on transactions Vol.E65-E No.7 pp.390-396

Publication Date: 1982/07/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Miscellaneous

Authors

Susumu YAMASAKI
Shuji DOSHITA

Keyword

Cite this

Copy

Susumu YAMASAKI, Shuji DOSHITA, "The Satisfiability Problems for Some Classes of Extended Horn Sets in the Propositional Logic" in IEICE TRANSACTIONS on transactions, vol. E65-E, no. 7, pp. 390-396, July 1982, doi: .
Abstract: The Horn set is the set of Horn clauses. The Horn clause is the set of literals which contains at most one positive literal, where a positive literal means a literal without negation sign. The satisfiability problem of the Horn set in propositional logic is one of P-complete problems, although the satisfiability problem of the formula in propositional logic is one of typical NP-complete problems. In propositional logic, unit and input resolutions, proposed by C. L. Chang, are complete inference rules used to detect the satisfiability of the Horn set. In this paper, we formulate a Restricted Linear (RL) deduction, extending unit and input resolutions. The RL deduction is formed by layering linear deductions each of which corresponds to an input resolution refutation, and is called by another name, a Linear Layered Resolution deduction based on Input resolution (an LLRI deduction). Next, we formulate a Nonlinear Layered Resolution deduction based on Input resolutions (an NLRI deduction). By means of the LLRI and NLRI deductions, we propose some classes of extended Horn sets in propositional logic for which the satisfiability problems are solvable by LLRI and NLRI deductions in deterministic polynomial time; and, thus, so are P-complete. Also we propose algorithms to determine whether a given set of clauses is in the proposed classes of extended Horn sets.
URL: https://global.ieice.org/en_transactions/transactions/10.1587/e65-e_7_390/_p

Copy

@ARTICLE{e65-e_7_390,
author={Susumu YAMASAKI, Shuji DOSHITA, },
journal={IEICE TRANSACTIONS on transactions},
title={The Satisfiability Problems for Some Classes of Extended Horn Sets in the Propositional Logic},
year={1982},
volume={E65-E},
number={7},
pages={390-396},
abstract={The Horn set is the set of Horn clauses. The Horn clause is the set of literals which contains at most one positive literal, where a positive literal means a literal without negation sign. The satisfiability problem of the Horn set in propositional logic is one of P-complete problems, although the satisfiability problem of the formula in propositional logic is one of typical NP-complete problems. In propositional logic, unit and input resolutions, proposed by C. L. Chang, are complete inference rules used to detect the satisfiability of the Horn set. In this paper, we formulate a Restricted Linear (RL) deduction, extending unit and input resolutions. The RL deduction is formed by layering linear deductions each of which corresponds to an input resolution refutation, and is called by another name, a Linear Layered Resolution deduction based on Input resolution (an LLRI deduction). Next, we formulate a Nonlinear Layered Resolution deduction based on Input resolutions (an NLRI deduction). By means of the LLRI and NLRI deductions, we propose some classes of extended Horn sets in propositional logic for which the satisfiability problems are solvable by LLRI and NLRI deductions in deterministic polynomial time; and, thus, so are P-complete. Also we propose algorithms to determine whether a given set of clauses is in the proposed classes of extended Horn sets.},
keywords={},
doi={},
ISSN={},
month={July},}

Copy

TY - JOUR
TI - The Satisfiability Problems for Some Classes of Extended Horn Sets in the Propositional Logic
T2 - IEICE TRANSACTIONS on transactions
SP - 390
EP - 396
AU - Susumu YAMASAKI
AU - Shuji DOSHITA
PY - 1982
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E65-E
IS - 7
JA - IEICE TRANSACTIONS on transactions
Y1 - July 1982
AB - The Horn set is the set of Horn clauses. The Horn clause is the set of literals which contains at most one positive literal, where a positive literal means a literal without negation sign. The satisfiability problem of the Horn set in propositional logic is one of P-complete problems, although the satisfiability problem of the formula in propositional logic is one of typical NP-complete problems. In propositional logic, unit and input resolutions, proposed by C. L. Chang, are complete inference rules used to detect the satisfiability of the Horn set. In this paper, we formulate a Restricted Linear (RL) deduction, extending unit and input resolutions. The RL deduction is formed by layering linear deductions each of which corresponds to an input resolution refutation, and is called by another name, a Linear Layered Resolution deduction based on Input resolution (an LLRI deduction). Next, we formulate a Nonlinear Layered Resolution deduction based on Input resolutions (an NLRI deduction). By means of the LLRI and NLRI deductions, we propose some classes of extended Horn sets in propositional logic for which the satisfiability problems are solvable by LLRI and NLRI deductions in deterministic polynomial time; and, thus, so are P-complete. Also we propose algorithms to determine whether a given set of clauses is in the proposed classes of extended Horn sets.
ER -