Focused Inductive Theorem Proving

13 years 5 months ago

Download www.lix.polytechnique.fr

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

David Baelde, Dale Miller, Zachary Snow

Real-time Traffic

CADE 2010 | Focused Proof | Logical Reasoning | Sequent Calculus Proofs | Systems Provide Means |

claim paper

» MatrixBased Inductive Theorem Proving

» Proof Search and Proof Check for Equational and Inductive Theorems

» How to Prove Inductive Theorems QUODLIBET

» From Proofs to Focused Proofs A Modular Proof of Focalization in Linear Logic

» Termination Analysis by Dependency Pairs and Inductive Theorem Proving

» An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving

» Sound Lemma Generation for Proving Inductive Validity of Equations

» Automated Theorem Proving in a Simple MetaLogic for LF

Post Info
More Details (n/a)

Added	08 Nov 2010
Updated	08 Nov 2010
Type	Conference
Year	2010
Where	CADE
Authors	David Baelde, Dale Miller, Zachary Snow

Comments (0)

Sciweavers

Focused Inductive Theorem Proving

CADE 2010 | Focused Proof | Logical Reasoning | Sequent Calculus Proofs | Systems Provide Means |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers