Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

32

TABLEAUX
2000
Springer

favoriteEmaildiscussreport

100views Artificial Intelligence» more TABLEAUX 2000»

Matrix-Based Inductive Theorem Proving

14 years 2 months ago

Matrix-Based Inductive Theorem Proving

Download www.nuprl.org

We present an approach to inductive theorem proving that integrates rippling-based rewriting into matrix-based logical proof search. The selection of appropriate connections in a matrix proof is guided by the symmetries between induction hypothesis and induction conclusion while unification is extended by a rippling/reverse-rippling heuristic. Conditional substitutions are generated whenever a uniform substitution is impossible. We illustrate the combined approach by discussing several inductive proofs for the integer square root problem.

Christoph Kreitz, Brigitte Pientka

Real-time Traffic

Artificial Intelligence | Inductive Theorem | Integer Square Root | Matrix-based Logical Proof | TABLEAUX 2000 |

claim paper

Related Content

» Using a Software Testing Technique to Improve Theorem Proving

» How to Prove Inductive Theorems QUODLIBET

» Termination Analysis by Dependency Pairs and Inductive Theorem Proving

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

» Focused Inductive Theorem Proving

» Sound Lemma Generation for Proving Inductive Validity of Equations

» Automated Theorem Proving in a Simple MetaLogic for LF

» History and Future of Implicit and Inductionless Induction Beware the Old Jade and the Zom...

» Proving theorems by reuse

Post Info
More Details (n/a)

Added	25 Aug 2010
Updated	25 Aug 2010
Type	Conference
Year	2000
Where	TABLEAUX
Authors	Christoph Kreitz, Brigitte Pientka

Comments (0)