A DPLL Procedure for the Propositional Product Logic

Dušan Guller

2013

Abstract

In the paper, we investigate the deduction problem of a formula from a finite theory in the propositional Product logic from a perspective of automated deduction.Our approach is based on the translation of a formula to an equivalent satisfiable finite order clausal theory, consisting of order clauses. An order clause is a finite set of order literals of the form $\varepsilon_1\diamond \varepsilon_2$ where $\varepsilon_i$ is either a conjunction of propositional atoms or the propositional constant $\gz$ (false) or $\gu$ (true), and $\diamond$ is a connective either $<$ or $=$. $<$ and $=$ are interpreted by the equality and standard strict linear order on $[0,1]$, respectively. A variant of the DPLL procedure, operating over order clausal theories, is proposed. The DPLL procedure is proved to be refutation sound and complete for finite order clausal theories.

Paper Citation

in Harvard Style

Guller D. (2013). A DPLL Procedure for the Propositional Product Logic . In Proceedings of the 5th International Joint Conference on Computational Intelligence - Volume 1: FCTA, (IJCCI 2013) ISBN 978-989-8565-77-8, pages 213-224. DOI: 10.5220/0004557402130224

in Bibtex Style

@conference{fcta13,
author={Dušan Guller},
title={A DPLL Procedure for the Propositional Product Logic},
booktitle={Proceedings of the 5th International Joint Conference on Computational Intelligence - Volume 1: FCTA, (IJCCI 2013)},
year={2013},
pages={213-224},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004557402130224},
isbn={978-989-8565-77-8},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 5th International Joint Conference on Computational Intelligence - Volume 1: FCTA, (IJCCI 2013)
TI - A DPLL Procedure for the Propositional Product Logic
SN - 978-989-8565-77-8
AU - Guller D.
PY - 2013
SP - 213
EP - 224
DO - 10.5220/0004557402130224