A Divergence Critic for Inductive Proof | Zendy

Toby Walsh | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Divergence Critic for Inductive Proof

Author(s) -

Toby Walsh

Publication year - 1996

Publication title -

journal of artificial intelligence research

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.79

H-Index - 123

eISSN - 1943-5037

pISSN - 1076-9757

DOI - 10.1613/jair.275

Subject(s) - mathematical proof , divergence (linguistics) , computer assisted proof , analytic proof , simple (philosophy) , computer science , proof complexity , matching (statistics) , proof of concept , automated theorem proving , inductive bias , calculus (dental) , mathematics , theoretical computer science , algorithm , task (project management) , medicine , philosophy , linguistics , statistics , geometry , multi task learning , management , epistemology , dentistry , economics , operating system

Inductive theorem provers often diverge. This paper describes a simple critic, a computer program which monitors the construction of inductive proofs attempting to identify diverging proof attempts. Divergence is recognized by means of a "difference matching" procedure. The critic then proposes lemmas and generalizations which "ripple" these differences away so that the proof can go through without divergence. The critic enables the theorem prover Spike to prove many theorems completely automatically from the definitions alone.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research