Settings for Refutational Theorem Proving

For refutational theorem proving, we have to find the right balance between forward computation (search) and simplification. A modest amount of simplification should be applied. A refutationally complete inference system is usually wanted. We get this automatically with the default settings of the system. We either call prove or else read a set of clauses (command in) containing the theory and the negation of the theorem to be proved, and then enter sat to invoke saturation. We recommend to use the lexicographic path ordering (default ordering) for refutational theorem proving. Then the definition of an ordering reduces to defining the precedences between the symbols (cf. in).

Imprint | Data Protection