Redirecting Proofs by Contradiction | Zendy

Jasmin Christian Blanchette | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Redirecting Proofs by Contradiction

Author(s) -

Jasmin Christian Blanchette

Publication year - 2018

Publication title -

epic series in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 2398-7340

DOI - 10.29007/wm8b

Subject(s) - mathematical proof , contradiction , natural deduction , computer science , gas meter prover , automated theorem proving , proof assistant , vampire , graph , calculus (dental) , discrete mathematics , algorithm , mathematics , programming language , theoretical computer science , philosophy , epistemology , medicine , geometry , dentistry

This paper presents an algorithm that redirects proofs by contradiction. The input is a refutation graph, as produced by an automatic theorem prover (e.g., E, SPASS, Vampire, Z3); the outputis a direct proofexpressedin naturaldeductionextendedwith case analyses and nested subproofs. The algorithm is implemented in Isabelle’s Sledgehammer, where it enhances the legibility of machine-generated proofs.

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