A Proof Procedure for the First Order Logic


Miodrag Kapetanović, Aleksandar Krapež


A new proof procedure is given for the classical predicate logic which combines variants of the tableaux and resolution methods. Soundness and completeness of the resulting system are proved.