More Web Proxy on the site http://driver.im/

research-article

Open access

Recording Completion for Certificates in Equational Reasoning

Authors:

Thomas Sternagel,

Harald ZanklAuthors Info & Claims

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

Pages 41 - 47

https://doi.org/10.1145/2676724.2693171

Published: 13 January 2015 Publication History

Abstract

We introduce recording completion, a variant of Knuth-Bendix completion which facilitates the construction of certificates for various equational logic proofs (completion proofs, entailment proofs and dis-proofs). The approach generalizes to more powerful variants of completion such as ordered completion and AC completion. We implemented recording completion in the tools KBCV and MKBTT. Both tools allow to choose among different formats of proof certificates, namely conversions, proof trees, and conversions with history. We report on experimental results in which all generated certificates have been verified by the trustable checker CeTA.

References

[1]

Franz Baader and Tobias Nipkow. Term Rewriting andtextitAll That. Cambridge University Press, New York, USA, August 1999.

Digital Library

[2]

Leo Bachmair, Nachum Dershowitz, and David Plaisted. Completion without failure. In Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, pages 1--30, 1989.

[3]

Garrett Birkhoff. On the structure of abstract algebras. Mathematical Proceedings of the Cambridge Philosophical Society, 31(4):433--454, 1935.

[4]

Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement day. In Jürgen Giesl and Reiner H\"ahnle, editors, IJCAR, volume 6173 of Lecture Notes in Artificial Intelligence, pages 107--121. Springer, 2010.

Digital Library

[5]

Evelyne Contejean and Pierre Corbineau. Reflecting proofs in first-order logic with equality. In Robert Nieuwenhuis, editor, CADE, volume 3632 of Lecture Notes in Artificial Intelligence, pages 7--22. Springer, 2005.

Digital Library

[6]

Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated certified proofs withCIME. In Manfred Schmidt-Schauß, editor, RTA, volume 10 of Leibniz International Proceedings in Informatics, pages 21--30. Schloss Dagstuhl, 2011.

[7]

Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, and Hendrik Spies. The Waldmeister loop at work. In CADE, volume 2741 of Lecture Notes in Artificial Intelligence, pages 317--321, 2003.

[8]

Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797--821, 1980.

Digital Library

[9]

Cezary Kaliszyk and Josef Urban. PRocH: Proof reconstruction for HOL light. In Maria Paola Bonacina, editor, CADE, volume 7898 of Lecture Notes in Artificial Intelligence, pages 267--274. Springer, 2013.

Digital Library

[10]

Donald E. Knuth and Peter P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263--297. Pergamon Press, New York, 1970.

[11]

Claude Marché. Normalized rewriting: An alternative to rewriting modulo a set of equations. J. Symb. Comp., 21(3):253--288, 1996.

Digital Library

[12]

William McCune and Olga Shumsky. Ivy: A preprocessor and proof checker for first-order logic. In Computer-Aided Reasoning: ACL2 Case Studies, chapter 16. Kluwer Academic Publishers, 2000.

Digital Library

[13]

Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233--264, 1981.

Digital Library

[14]

David Plaisted and Andrea Sattler-Klein. Proof lengths for equational completion. Information and Computation, 125(2):154--170, 1996.

Digital Library

[15]

Christian Sternagel and René Thiemann. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In Femke van Raamsdonk, editor, RTA, volume 21 of Leibniz International Proceedings in Informatics, pages 287--302. Schloss Dagstuhl, 2013.

[16]

Thomas Sternagel and Harald Zankl. KBCV -- Knuth-Bendix completion visualizer. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, IJCAR, volume 7364 of Lecture Notes in Artificial Intelligence, pages 530--536, 2012.

Digital Library

[17]

Geoff Sutcliffe. Semantic derivation verification. Int. J. Artif. Intell. Tools, 15(6):1053--1070, 2006.

[18]

René Thiemann and Christian Sternagel. Certification of termination proofs using CETA. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs, volume 5674 of Lecture Notes in Computer Science, pages 452--468. Springer, 2009.

Digital Library

[19]

Ian Wehrman and Aaron Stump. Mining propositional simplification proofs for small validating clauses. In Proc. 3rd PDPAR, volume 144 of ENTCS, pages 79--91, 2005.

Digital Library

[20]

Ian Wehrman, Aaron Stump, and Edwin M. Westbrook. Slothrop: Knuth-Bendix completion with a modern termination checker. In Frank Pfenning, editor, RTA, volume 4098 of Lecture Notes in Computer Science, pages 287--296. Springer, 2006.

Digital Library

[21]

Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara. Multi-completion with termination tools. J. Autom. Reasoning, 50(3):317--354, 2013.

Digital Library

Cited By

Sternagel CWinkler S(2019)Certified Equational Reasoning via Ordered CompletionAutomated Deduction – CADE 2710.1007/978-3-030-29436-6_30(508-525)Online publication date: 20-Aug-2019
https://doi.org/10.1007/978-3-030-29436-6_30
Winkler SMoser G(2018)MædMax: A Maximal Ordered Completion ToolAutomated Reasoning10.1007/978-3-319-94205-6_31(472-480)Online publication date: 30-Jun-2018
https://doi.org/10.1007/978-3-319-94205-6_31
Chihani ZMiller D(2016)Proof Certificates for Equality ReasoningElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.06.007323:C(93-108)Online publication date: 11-Jul-2016
https://dl.acm.org/doi/10.1016/j.entcs.2016.06.007

Index Terms

Recording Completion for Certificates in Equational Reasoning
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Sound and Complete Equational Reasoning over Comodels

Comodels of Lawvere theories, i.e. models in Setop, model state spaces with algebraic access operations. Standard equational reasoning is known to be sound but incomplete for comodels. We give two sound and complete calculi for equational reasoning over ...
Certified Equational Reasoning via Ordered Completion
Automated Deduction – CADE 27
Abstract
On the one hand, equational reasoning is a fundamental part of automated theorem proving with ordered completion as a key technique. On the other hand, the complexity of corresponding, often highly optimized, automated reasoning tools makes ...
Diagrammatic Confluence and Completion
ICALP '09: Proceedings of the 36th Internatilonal Collogquium on Automata, Languages and Programming: Part II

We give a new elegant proof that decreasing diagrams imply confluence based on a proof reduction technique, which is then the basis of a novel completion method which proof-reduction relation transforms arbitrary proofs into rewrite proofs even in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

January 2015

192 pages

ISBN:9781450332965

DOI:10.1145/2676724

Program Chairs:
Xavier Leroy
Inria Paris-Rocquencourt, France
,
Alwen Tiu
Nanyang Technological University, Singapore

Copyright © 2015 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 January 2015

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Austrian Science Fund

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 13 - 14, 2015

Mumbai, India

Acceptance Rates

CPP '15 Paper Acceptance Rate 18 of 26 submissions, 69%;

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
279
Total Downloads

Downloads (Last 12 months)38
Downloads (Last 6 weeks)7

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sternagel CWinkler S(2019)Certified Equational Reasoning via Ordered CompletionAutomated Deduction – CADE 2710.1007/978-3-030-29436-6_30(508-525)Online publication date: 20-Aug-2019
https://doi.org/10.1007/978-3-030-29436-6_30
Winkler SMoser G(2018)MædMax: A Maximal Ordered Completion ToolAutomated Reasoning10.1007/978-3-319-94205-6_31(472-480)Online publication date: 30-Jun-2018
https://doi.org/10.1007/978-3-319-94205-6_31
Chihani ZMiller D(2016)Proof Certificates for Equality ReasoningElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2016.06.007323:C(93-108)Online publication date: 11-Jul-2016
https://dl.acm.org/doi/10.1016/j.entcs.2016.06.007

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents