Protein: A PROver with a Theory Extension INterface
P Baumgartner, U Furbach - International Conference on Automated …, 1994 - Springer
International Conference on Automated Deduction, 1994•Springer
PROTEIN (PRO ver with a T heory E xtension IN terface) is a PTTP-based first order theorem
prover over built-in theories. Besides various standard-refinements known for model
elimination, PROTEIN also offers a variant of model elimination for case-based reasoning
and which does not need contrapositives.
prover over built-in theories. Besides various standard-refinements known for model
elimination, PROTEIN also offers a variant of model elimination for case-based reasoning
and which does not need contrapositives.
Abstract
PROTEIN (PROver with a Theory Extension INterface) is a PTTP-based first order theorem prover over built-in theories. Besides various standard-refinements known for model elimination, PROTEIN also offers a variant of model elimination for case-based reasoning and which does not need contrapositives.
Springer