2 papers
math.GM2004
First-Order Intuitionistic Logic with Decidable Propositional Atoms
Alexander Sakharov
Intuitionistic logic extended with decidable propositional atoms combines classical properties in its propositional part and intuitionistic properties for derivable formulas not co…
cs.LO2003
A Transformational Decision Procedure for Non-Clausal Propositional Formulas
Alexander Sakharov
A decision procedure for detecting valid propositional formulas is presented. It is based on the Davis-Putnam method and deals with propositional formulas that are initially conver…