EasyChair Publications
Search
Paper Information
Paper:Jasmin Christian Blanchette
Redirecting Proofs by Contradiction
Title:Redirecting Proofs by Contradiction
Authors:Jasmin Christian Blanchette
Keyphrases:resolution, direct proofs, automatic theorem provers, proof assistants, isabelle/hol, sledgehammer
Paper:
Abstract: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 output is a direct proof expressed in natural deduction extended with case analyses and nested subproofs. The algorithm is implemented in Isabelle’s Sledgehammer, where it enhances the legibility of machine-generated proofs.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:11-26
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:12
Downloads:15
BibTeX entry:
@inproceedings{PxTP2013:Redirecting_Proofs_by_Contradiction,
  author    = {Jasmin Christian Blanchette},
  title     = {Redirecting Proofs by Contradiction},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {11-26},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}