First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
From MaRDI portal
Publication:6103588
DOI10.1007/s10817-023-09661-7MaRDI QIDQ6103588
Fabian Mitterwallner, Aart Middeldorp, Alexander Lochmann
Publication date: 27 June 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Reachability, confluence, and termination analysis with state-compatible automata
- A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
- Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems
- The first-order theory of linear one-step rewriting is undecidable
- Decidability for left-linear growing term rewriting systems.
- Decidable call-by-need computations in term rewriting
- FORT 2.0
- Sequentiality, monadic second-order logic and tree automata.
- The undecidability of the first-order theories of one step rewriting in linear canonical systems
- Certifying proofs in the first-order theory of rewriting
- Foundations of software science and computation structures. 8th international conference, FOSSACS 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4--8, 2005. Proceedings.
- CSI: new evidence -- a progress report
- Tools and algorithms for the construction and analysis of systems. 25 years of TACAS: TOOLympics, held as part of ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings. Part III
- MONA IMPLEMENTATION SECRETS
- Turning Inductive into Equational Specifications
- Certification of Termination Proofs Using CeTA
- CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
- Proving Confluence of Term Rewriting Systems Automatically
- Finding small counterexamples for abstract rewriting properties
- Undecidability of the first order theory of one-step right ground rewriting
- Term Rewriting and All That
- A Rewriting View of Simple Typing
- Open problems in rewriting
- Polynomial time termination and constraint satisfaction tests
- Deciding Confluence of Ground Term Rewrite Systems in Cubic Time.
- Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
- Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
- Ground Confluence Prover based on Rewriting Induction
- Computer Science Logic
- The First-Order Theory of Ground Tree Rewrite Graphs
- Termination of Rewriting with Right-Flat Rules
