PROTEIN: A PROver with a Theory Extension INterface

Abstract. PROTEIN (PROver with a Theory Extension INterface) is a PTTPbased first order theorem prover over built-in theories. Besides various standardrefinements knownformodelelimination,PROTEIN alsooffers a variantofmodel elimination for case-based reasoning and which does not need contrapositives. PROTEIN is a complete theorem prover for first order clause logic. It is characterized by the following features:

• Type: Conference
• Year: 1994
• Where: CADE
• Authors: Peter Baumgartner, Ulrich Furbach
• Keywords: CADE 1994, Logical Reasoning, Order Theorem Prover, Protein, Theorem Provers