DE ITA LUNA, GUILLERMO; MARCIAL ROMERO, JOSE RAYMUNDO; HERNANDEZ SERVIN, JOSE ANTONIO
(ELSEVIER, 2016-01-01)
We propose a novel method to review K ⊢ φ when K and φ are both in Conjunctive Normal Forms (CF). We extend our method to solve the incremental satisfiablity problem (ISAT), and we present different cases where ISAT can ...