Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms.

Hans de Nivelle

Published in: CADE (2003)

Keyphrases

first order logic
theorem prover
theorem proving
horn clauses
formal proofs
high resolution
higher order
consequence finding
equational theories
low resolution
database
information systems
machine translation