Focused Inductive Theorem Proving

Abstract. Focused proof systems provide means for reducing and structuring the non-determinism involved in searching for sequent calculus proofs. We present a focused proof system for a first-order logic with in

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: David Baelde, Dale Miller, Zachary Snow
• Keywords: CADE 2010, Focused Proof, Logical Reasoning, Sequent Calculus Proofs, Systems Provide Means