The Markgraf Karl Refutation Procedure PLL: a First-Order Language for an Automated Theorem Prover

Abstract

The PREDICATE LOGIC LANGUAGE (PLL), a formal language in which first-order predicate logic formulas are formulated, is described. In PLL axioms and theorems are represented which are given to the MARKGRAF KARL REFUTATION PROCEDURE. Certain expressions of PLL which reflect the special facilities of this system are exhibited, viz. - an inference mechanism based on a many-sorted calculus, - the incorporation of special axioms into the inference mechanism, and - the control of the inference mechanism using special derivation strategies.