Hyperresolution for Propositional Product Logic

Dušan Guller

2016

Abstract

We provide the foundations of automated deduction in the propositional product logic. Particularly, we generalise the hyperresolution principle for the propositional product logic. We propose translation of a formula to an equivalent satisfiable finite order clausal theory, which consists of order clauses - finite sets of order literals of the augmented form: e1 @ e2 where e1 is either a truth constant, 0, 1, or a conjunction of powers of propositional atoms, and @ is a connective from =, <. = and < are interpreted by the equality and strict linear order on [0,1], respectively. We devise a hyperresolution calculus over order clausal theories, which is refutation sound and complete for the finite case. By means of the translation and calculus, we solve the deduction problem T |= phi for a finite theory T and a formula phi.

Paper Citation

in Harvard Style

Guller D. (2016). Hyperresolution for Propositional Product Logic . In Proceedings of the 8th International Joint Conference on Computational Intelligence - Volume 2: FCTA, (IJCCI 2016) ISBN 978-989-758-201-1, pages 30-41. DOI: 10.5220/0006044300300041

in Bibtex Style

@conference{fcta16,
author={Dušan Guller},
title={Hyperresolution for Propositional Product Logic},
booktitle={Proceedings of the 8th International Joint Conference on Computational Intelligence - Volume 2: FCTA, (IJCCI 2016)},
year={2016},
pages={30-41},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0006044300300041},
isbn={978-989-758-201-1},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 8th International Joint Conference on Computational Intelligence - Volume 2: FCTA, (IJCCI 2016)
TI - Hyperresolution for Propositional Product Logic
SN - 978-989-758-201-1
AU - Guller D.
PY - 2016
SP - 30
EP - 41
DO - 10.5220/0006044300300041