First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification. (English) Zbl 07702720
MSC:
68V15
Found 18 Documents (Results 1–18)
Term orderings for non-reachability of (conditional) rewriting. (English) Zbl 07628191
Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 248-267 (2022).
MSC:
68V15
Use of logical models for proving infeasibility in term rewriting. (English) Zbl 1477.68140
MSC:
68Q42
Context-sensitive dependency pairs. (English) Zbl 1206.68158
MSC:
68Q42
Match-bounds revisited. (English) Zbl 1192.68399
MSC:
68Q42
Beyond dependency graphs. (English) Zbl 1250.68143
Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 339-354 (2009).
MSC:
68Q42
68T15
Match-bounds with dependency pairs for proving termination of rewrite systems. (English) Zbl 1156.68430
Martín-Vide, Carlos (ed.) et al., Language and automata theory and applications. Second international conference, LATA 2008, Tarragona, Spain, March 13–19, 2008. Revised papers. Berlin: Springer (ISBN 978-3-540-88281-7/pbk). Lecture Notes in Computer Science 5196, 321-332 (2008).
Enhancing dependency pair method using strong computability in simply-typed term rewriting. (English) Zbl 1125.68064
Mechanizing and improving dependency pairs. (English) Zbl 1113.68088
MSC:
68T15
68Q42
Elimination transformations for associative-commutative rewriting systems. (English) Zbl 1113.68059
MSC:
68Q42
68T15
Deciding \(\mathcal H_1\) by resolution. (English) Zbl 1185.68620
MSC:
68T15
68Q45
Automating the dependency pair method. (English) Zbl 1081.68038
MSC:
68Q42
Modular and incremental automated termination proofs. (English) Zbl 1096.68076
MSC:
68Q42
68T15
Modular termination proofs for rewriting using dependency pairs. (English) Zbl 1010.68073
MSC:
68Q42
Hierarchical termination revisited. (English) Zbl 1042.68602
MSC:
68Q05
68Q42
Filter Results by …
Document Type
- Journal Articles (15)
- Collection Articles (3)
all
top 5
Author
- Middeldorp, Aart (6)
- Korp, Martin (3)
- Lucas, Salvador (3)
- Gutiérrez, Raúl (2)
- Urbain, Xavier (2)
- Alarcón, Beatriz (1)
- Contejean, Evelyne (1)
- Durand, Irène A. (1)
- Falke, Stephan (1)
- Giesl, Jürgen (1)
- Goubault-Larrecq, Jean (1)
- Hirokawa, Nao (1)
- Keiichirou, Kusakari (1)
- Kusakari, Keiichirou (1)
- Lochmann, Alexander (1)
- Marché, Claude (1)
- Masaki, Nakamura (1)
- Mitterwallner, Fabian (1)
- Ohlebusch, Enno (1)
- Ohlebusch, Jürgen Gieslthomas Artsenno (1)
- Sakai, Masahiko (1)
- Schneider-Kamp, Peter (1)
- Thiemann, René (1)
- Tomás, Ana Paula (1)
- Yamada, Akihisa (1)
- Yoshihito, Toyama (1)
all
top 5
Serial
- J. Autom. Reasoning (5)
- Inf. Comput. (4)
- Inf. Process. Lett. (3)
- Artif. Intell. (1)
- J. Symb. Comput. (1)
- Appl. Algebra Eng. Commun. Comput. (1)
all
top 3
Software
- AProVE (9)
- Tyrolean (6)
- Tsukuba (3)
- Haskell (2)
- MU-TERM (2)
- Mace4 (2)
- Matchbox (2)
- Maude (2)
- Prover9 (2)
- AGES (1)
- Archive Formal Proofs (1)
- Autowrite (1)
- CARIBOO (1)
- CLEAN (1)
- CSDP (1)
- CSI (1)
- CeTA (1)
- CiME (1)
- CoLL (1)
- Conditional Confluence (1)
- FOL Fitting (1)
- FORT (1)
- ITP (1)
- Isabelle/HOL (1)
- Jambox (1)
- ML (1)
- MONA (1)
- Mercury (1)
- Mizar (1)
- ModGen (1)
- NaTT (1)
- Nagoya Termination Tool (1)
- OBJ3 (1)
- REVE (1)
- StarExec (1)
- TALP (1)
- TPA (1)
- Timbuk (1)
- VMTL (1)
- infChecker (1)
- z3 (1)
