LIPIcs.FSCD.2018.31.pdf
- Filesize: 0.54 MB
- 8 pages
Document
ProTeM: A Proof Term Manipulator (System Description)
Authors
Christina Kohl 
,
Aart Middeldorp
-
Part of:
Volume:
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-07-04
File
Document Identifiers
Author Details
Cite As Get BibTex
Christina Kohl and Aart Middeldorp. ProTeM: A Proof Term Manipulator (System Description). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 31:1-31:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.31
Abstract
Proof terms are a useful concept for reasoning about computations in term rewriting. Human calculation with proof terms is tedious and error-prone. We present ProTeM, a new tool that offers support for manipulating proof terms that represent multisteps in left-linear rewrite systems.
Subject Classification
ACM Subject Classification
- Theory of computation → Rewrite systems
- Theory of computation → Equational logic and rewriting
Keywords
- Proof terms
- term rewriting
- interactive tool
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
H.J. Sander Bruggink. Equivalence of Reductions in Higher-Order Rewriting. PhD thesis, Utrecht University, 2008.
- Nao Hirokawa and Aart Middeldorp. Decreasing diagrams and relative termination. Journal of Automated Reasoning, 47(4):481-501, 2011. URL: http://dx.doi.org/10.1007/s10817-011-9238-x.
-
Nao Hirokawa and Aart Middeldorp. Commutation via relative termination. In Proc. 2nd International Workshop on Confluence, pages 29-33, 2013.
- Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797-821, 1980. URL: http://dx.doi.org/10.1145/322217.322230.
- Carlos Lombardi, Alejandro Ríos, and Roel de Vrijer. Proof terms for infinitary rewriting. In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of Lecture Notes in Computer Science (Advanced Research in Computing and Software Science), pages 303-318, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08918-8_21.
- Claude Marché, Albert Rubio, and Hans Zantema. Termination problem data base: Format of input files. https://www.lri.fr/~marche/tpdb/format.html. Accessed: 2018-17-01.
-
Julian Nagele. Mechanizing Confluence. PhD thesis, University of Innsbruck, 2017.
- Julian Nagele and Aart Middeldorp. Certification of classical confluence results for left-linear term rewrite systems. In Proc. 7th International Conference on Interactive Theorem Proving, volume 9807 of Lecture Notes in Computer Science, pages 290-306, 2016. URL: http://dx.doi.org/10.1007/978-3-319-43144-4_18.
-
Terese, editor. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
- Vaadin framework 8. https://vaadin.com/docs/v8/framework/introduction/intro-overview.html. Accessed: 2018-17-01.
- Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00173-9.
- Vincent van Oostrom and Roel de Vrijer. Four equivalent equivalences of reductions. In Proc. 2nd International Workshop on Reduction Strategies in Rewriting and Programming, volume 70(6) of Electronic Notes in Theoretical Computer Science, pages 21-61, 2002. URL: http://dx.doi.org/10.1016/S1571-0661(04)80599-1.