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.
|