default search action
Aart Middeldorp
Person information
- affiliation: University of Innsbruck, Austria
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j41]René Thiemann, Fabian Mitterwallner, Aart Middeldorp:
Undecidability Results on Orienting Single Rewrite Rules. Arch. Formal Proofs 2024 (2024) - [c103]Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp:
Confluence of Logically Constrained Rewrite Systems Revisited. IJCAR (2) 2024: 298-316 - [c102]Fabian Mitterwallner, Aart Middeldorp, René Thiemann:
Linear Termination is Undecidable. LICS 2024: 57:1-57:12 - [i14]Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp:
Confluence of Logically Constrained Rewrite Systems Revisited. CoRR abs/2402.13552 (2024) - [i13]Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp:
Left-Linear Completion with AC Axioms. CoRR abs/2405.17109 (2024) - 2023
- [j40]Aart Middeldorp, Alexander Lochmann, Fabian Mitterwallner:
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification. J. Autom. Reason. 67(2): 14 (2023) - [c101]Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp:
Left-Linear Completion with AC Axioms. CADE 2023: 401-418 - [c100]Jonas Schöpf, Aart Middeldorp:
Confluence Criteria for Logically Constrained Rewrite Systems. CADE 2023: 474-490 - [c99]Christina Kohl, Aart Middeldorp:
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. CPP 2023: 197-210 - [c98]Nao Hirokawa, Aart Middeldorp:
Hydra Battles and AC Termination. FSCD 2023: 12:1-12:16 - [c97]Christina Kohl, Aart Middeldorp:
Formalizing Almost Development Closed Critical Pairs (Short Paper). ITP 2023: 38:1-38:8 - [i12]Nao Hirokawa, Aart Middeldorp:
Hydra Battles and AC Termination, Revisited. CoRR abs/2307.14036 (2023) - [i11]Fabian Mitterwallner, Aart Middeldorp, René Thiemann:
Linear Termination over N is Undecidable. CoRR abs/2307.14805 (2023) - [i10]Jonas Schöpf, Aart Middeldorp:
Confluence Criteria for Logically Constrained Rewrite Systems (Full Version). CoRR abs/2309.12112 (2023) - 2022
- [c96]Fabian Mitterwallner, Aart Middeldorp:
Polynomial Termination Over ℕ Is Undecidable. FSCD 2022: 27:1-27:17 - 2021
- [j39]Aart Middeldorp, Julian Nagele, Kiraku Shintani:
CoCo 2019: report on the eighth confluence competition. Int. J. Softw. Tools Technol. Transf. 23(6): 905-916 (2021) - [c95]Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer:
A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. CPP 2021: 250-263 - [c94]Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer:
Certifying Proofs in the First-Order Theory of Rewriting. TACAS (2) 2021: 127-144 - 2020
- [c93]Alexander Lochmann, Aart Middeldorp:
Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting. TACAS (2) 2020: 178-194
2010 – 2019
- 2019
- [j38]Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler:
Abstract Completion, Formalized. Log. Methods Comput. Sci. 15(3) (2019) - [c92]Christina Kohl, Aart Middeldorp:
Composing Proof Terms. CADE 2019: 337-353 - [c91]Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp:
A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. CPP 2019: 132-143 - [c90]Aart Middeldorp, Julian Nagele, Kiraku Shintani:
Confluence Competition 2019. TACAS (3) 2019: 25-40 - [c89]Sarah Winkler, Aart Middeldorp:
Tools in Term Rewriting for Education. ThEdu@CADE 2019: 54-72 - 2018
- [c88]Franziska Rapp, Aart Middeldorp:
FORT 2.0. IJCAR 2018: 81-88 - [c87]Nao Hirokawa, Julian Nagele, Aart Middeldorp:
Cops and CoCoWeb: Infrastructure for Confluence Tools. IJCAR 2018: 346-353 - [c86]Sarah Winkler, Aart Middeldorp:
Completion for Logically Constrained Rewriting. FSCD 2018: 30:1-30:18 - [c85]Christina Kohl, Aart Middeldorp:
ProTeM: A Proof Term Manipulator (System Description). FSCD 2018: 31:1-31:8 - [c84]Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, Harald Zankl:
Confluence Competition 2018. FSCD 2018: 32:1-32:5 - [i9]Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler:
Abstract Completion, Formalized. CoRR abs/1802.08437 (2018) - 2017
- [j37]Cynthia Kop, Aart Middeldorp, Thomas Sternagel:
Complexity of Conditional Term Rewriting. Log. Methods Comput. Sci. 13(1) (2017) - [j36]Amy P. Felty, Aart Middeldorp:
Preface: Selected Extended Papers of CADE 2015. J. Autom. Reason. 58(3): 311-312 (2017) - [c83]Julian Nagele, Bertram Felgenhauer, Aart Middeldorp:
CSI: New Evidence - A Progress Report. CADE 2017: 385-397 - [c82]Bertram Felgenhauer, Aart Middeldorp:
Constructing Cycles in the Simplex Method for DPLL(T). ICTAC 2017: 213-228 - [c81]Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler:
Infinite Runs in Abstract Completion. FSCD 2017: 19:1-19:16 - [i8]Julian Nagele, Aart Middeldorp:
CoCoWeb - A Convenient Web Interface for Confluence Tools. CoRR abs/1708.07876 (2017) - 2016
- [j35]Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
AC-KBO revisited. Theory Pract. Log. Program. 16(2): 163-188 (2016) - [c80]Julian Nagele, Aart Middeldorp:
Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. ITP 2016: 290-306 - [c79]Franziska Rapp, Aart Middeldorp:
Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems. FSCD 2016: 36:1-36:12 - 2015
- [j34]Harald Zankl, Bertram Felgenhauer, Aart Middeldorp:
Labelings for Decreasing Diagrams. J. Autom. Reason. 54(2): 101-133 (2015) - [j33]Harald Zankl, Sarah Winkler, Aart Middeldorp:
Beyond polynomials and Peano arithmetic - automation of elementary and ordinal interpretations. J. Symb. Comput. 69: 129-158 (2015) - [j32]Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, Vincent van Oostrom:
Layer Systems for Proving Confluence. ACM Trans. Comput. Log. 16(2): 14:1-14:32 (2015) - [c78]Nao Hirokawa, Aart Middeldorp, Georg Moser:
Leftmost Outermost Revisited. RTA 2015: 209-222 - [c77]Cynthia Kop, Aart Middeldorp, Thomas Sternagel:
Conditional Complexity. RTA 2015: 223-240 - [c76]Julian Nagele, Bertram Felgenhauer, Aart Middeldorp:
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. RTA 2015: 257-268 - [e8]Amy P. Felty, Aart Middeldorp:
Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Lecture Notes in Computer Science 9195, Springer 2015, ISBN 978-3-319-21400-9 [contents] - [e7]Aart Middeldorp, Femke van Raamsdonk:
Proceedings 8th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2014, Vienna, Austria, July 13, 2014. EPTCS 183, 2015 [contents] - 2014
- [j31]Friedrich Neurauter, Aart Middeldorp:
Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited. Log. Methods Comput. Sci. 10(3) (2014) - [c75]Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
AC-KBO Revisited. FLOPS 2014: 319-335 - [c74]Nao Hirokawa, Aart Middeldorp, Christian Sternagel:
A New and Formalized Proof of Abstract Completion. ITP 2014: 292-307 - [c73]Thomas Sternagel, Aart Middeldorp:
Conditional Confluence (System Description). RTA-TLCA 2014: 456-465 - [e6]Kenneth L. McMillan, Aart Middeldorp, Geoff Sutcliffe, Andrei Voronkov:
LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings. EPiC Series in Computing 26, EasyChair 2014 [contents] - [i7]Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp:
AC-KBO Revisited. CoRR abs/1403.0406 (2014) - [i6]Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, Vincent van Oostrom:
Layer Systems for Proving Confluence. CoRR abs/1404.1225 (2014) - [i5]Harald Zankl, Bertram Felgenhauer, Aart Middeldorp:
Labelings for Decreasing Diagrams. CoRR abs/1406.3139 (2014) - 2013
- [j30]Nao Hirokawa, Aart Middeldorp, Harald Zankl:
Uncurrying for Termination and Complexity. J. Autom. Reason. 50(3): 279-315 (2013) - [j29]Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara:
Multi-Completion with Termination Tools. J. Autom. Reason. 50(3): 317-354 (2013) - [c72]Sarah Winkler, Aart Middeldorp:
Normalized Completion Revisited. RTA 2013: 319-334 - [c71]Sarah Winkler, Harald Zankl, Aart Middeldorp:
Beyond Peano Arithmetic - Automatically Proving Termination of the Goodstein Sequence. RTA 2013: 335-351 - [e5]Kenneth L. McMillan, Aart Middeldorp, Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. Lecture Notes in Computer Science 8312, Springer 2013, ISBN 978-3-642-45220-8 [contents] - 2012
- [j28]Takahito Aoto, Aart Middeldorp:
Preface. Theor. Comput. Sci. 464: 1-2 (2012) - [c70]Aart Middeldorp:
Matrix Interpretations for Polynomial Derivational Complexity of Rewrite Systems. LPAR 2012: 12 - [c69]Friedrich Neurauter, Aart Middeldorp:
On the Domain and Dimension Hierarchy of Matrix Interpretations. LPAR 2012: 320-334 - [c68]Sarah Winkler, Harald Zankl, Aart Middeldorp:
Ordinals and Knuth-Bendix Orders. LPAR 2012: 420-434 - 2011
- [j27]Nao Hirokawa, Aart Middeldorp:
Decreasing Diagrams and Relative Termination. J. Autom. Reason. 47(4): 481-501 (2011) - [c67]Sarah Winkler, Aart Middeldorp:
AC Completion with Termination Tools. CADE 2011: 492-498 - [c66]Harald Zankl, Bertram Felgenhauer, Aart Middeldorp:
CSI - A Confluence Tool. CADE 2011: 499-505 - [c65]Aart Middeldorp, Georg Moser, Friedrich Neurauter, Johannes Waldmann, Harald Zankl:
Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems. CAI 2011: 1-20 - [c64]Bertram Felgenhauer, Harald Zankl, Aart Middeldorp:
Layer Systems for Proving Confluence. FSTTCS 2011: 288-299 - [c63]Friedrich Neurauter, Aart Middeldorp:
Revisiting Matrix Interpretations for Proving Termination of Term Rewriting. RTA 2011: 251-266 - [c62]Harald Zankl, Bertram Felgenhauer, Aart Middeldorp:
Labelings for Decreasing Diagrams. RTA 2011: 377-392 - 2010
- [c61]Nao Hirokawa, Aart Middeldorp:
Decreasing Diagrams and Relative Termination. IJCAR 2010: 487-501 - [c60]Friedrich Neurauter, Aart Middeldorp, Harald Zankl:
Monotonicity Criteria for Polynomial Interpretations over the Naturals. IJCAR 2010: 502-517 - [c59]Sarah Winkler, Aart Middeldorp:
Termination Tools in Ordered Completion. IJCAR 2010: 518-532 - [c58]Harald Zankl, Aart Middeldorp:
Satisfiability of Non-linear (Ir)rational Arithmetic. LPAR (Dakar) 2010: 481-500 - [c57]Friedrich Neurauter, Harald Zankl, Aart Middeldorp:
Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting. LPAR (Yogyakarta) 2010: 550-564 - [c56]Friedrich Neurauter, Aart Middeldorp:
Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers. RTA 2010: 243-258 - [c55]Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara:
Optimizing mkbTT. RTA 2010: 373-384 - [c54]Harald Zankl, Christian Sternagel, Dieter Hofbauer, Aart Middeldorp:
Finding and Certifying Loops. SOFSEM 2010: 755-766 - [c53]Harald Zankl, Nao Hirokawa, Aart Middeldorp:
Uncurrying for Innermost Termination and Derivational Complexity. HOR 2010: 46-57
2000 – 2009
- 2009
- [j26]Harald Zankl, Aart Middeldorp:
Increasing interpretations. Ann. Math. Artif. Intell. 56(1): 87-108 (2009) - [j25]Martin Korp, Aart Middeldorp:
Match-bounds revisited. Inf. Comput. 207(11): 1259-1283 (2009) - [j24]Haruhiko Sato, Masahito Kurihara, Sarah Winkler, Aart Middeldorp:
Constraint-Based Multi-Completion Procedures for Term Rewriting Systems. IEICE Trans. Inf. Syst. 92-D(2): 220-234 (2009) - [j23]Harald Zankl, Nao Hirokawa, Aart Middeldorp:
KBO Orientability. J. Autom. Reason. 43(2): 173-201 (2009) - [c52]Martin Korp, Aart Middeldorp:
Beyond Dependency Graphs. CADE 2009: 339-354 - [c51]Martin Korp, Christian Sternagel, Harald Zankl, Aart Middeldorp:
Tyrolean Termination Tool 2. RTA 2009: 295-304 - [e4]Aart Middeldorp:
Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming, WRS@RTA 2008, Hagenberg, Austria, July 14, 2008. Electronic Notes in Theoretical Computer Science 237, Elsevier 2009 [contents] - [i4]Irène Durand, Aart Middeldorp:
On the Complexity of Deciding Call-by-Need. CoRR abs/0901.0869 (2009) - [i3]Nao Hirokawa, Aart Middeldorp:
Decreasing Diagrams and Relative Termination. CoRR abs/0910.2853 (2009) - 2008
- [c50]Harald Zankl, Aart Middeldorp:
Increasing Interpretations. AISC/MKM/Calculemus 2008: 191-205 - [c49]Haruhiko Sato, Sarah Winkler, Masahito Kurihara, Aart Middeldorp:
Multi-completion with Termination Tools (System Description). IJCAR 2008: 306-312 - [c48]Martin Korp, Aart Middeldorp:
Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems. LATA 2008: 321-332 - [c47]Nao Hirokawa, Aart Middeldorp, Harald Zankl:
Uncurrying for Termination. LPAR 2008: 667-681 - [c46]Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl:
Maximal Termination. RTA 2008: 110-125 - [c45]Christian Sternagel, Aart Middeldorp:
Root-Labeling. RTA 2008: 336-350 - [c44]Aart Middeldorp:
Preface. WRS@RTA 2008: 1-2 - [c43]Harald Zankl, Christian Sternagel, Aart Middeldorp:
Transforming SAT into Termination of Rewriting. WFLP 2008: 199-214 - 2007
- [j22]Nao Hirokawa, Aart Middeldorp:
Tyrolean termination tool: Techniques and features. Inf. Comput. 205(4): 474-511 (2007) - [c42]Adam Koprowski, Aart Middeldorp:
Predictive Labeling with Dependency Pairs Using SAT. CADE 2007: 410-425 - [c41]Martin Korp, Aart Middeldorp:
Proving Termination of Rewrite Systems Using Bounds. RTA 2007: 273-287 - [c40]Harald Zankl, Aart Middeldorp:
Satisfying KBO Constraints. RTA 2007: 389-403 - [c39]Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl:
SAT Solving for Termination Analysis with Polynomial Interpretations. SAT 2007: 340-354 - [c38]Harald Zankl, Nao Hirokawa, Aart Middeldorp:
Constraints for Argument Filterings. SOFSEM (1) 2007: 579-590 - [c37]René Thiemann, Aart Middeldorp:
Innermost Termination of Rewrite Systems by Labeling. WRS@RDP 2007: 3-19 - [i2]Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, Harald Zankl:
Implementing RPO and POLO using SAT. Deduction and Decision Procedures 2007 - 2006
- [c36]Nao Hirokawa, Aart Middeldorp:
Predictive Labeling. RTA 2006: 313-327 - [i1]Harald Zankl, Aart Middeldorp:
Satisfying KBO Constraints. CoRR abs/cs/0608032 (2006) - 2005
- [j21]Irène Durand, Aart Middeldorp:
Decidable call-by-need computations in term rewriting. Inf. Comput. 196(2): 95-126 (2005) - [j20]Nao Hirokawa, Aart Middeldorp:
Automating the dependency pair method. Inf. Comput. 199(1-2): 172-199 (2005) - [c35]Nao Hirokawa, Aart Middeldorp:
Tyrolean Termination Tool. RTA 2005: 175-184 - [e3]Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, Roel C. de Vrijer:
Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 3838, Springer 2005, ISBN 3-540-30911-X [contents] - 2004
- [j19]Jürgen Giesl, Aart Middeldorp:
Transformation techniques for context-sensitive rewrite systems. J. Funct. Program. 14(4): 379-427 (2004) - [c34]Nao Hirokawa, Aart Middeldorp:
Polynomial Interpretations with Negative Coefficients. AISC 2004: 185-198 - [c33]Mircea Marin, Aart Middeldorp:
New completeness results for lazy conditional narrowing. PPDP 2004: 120-131 - [c32]Nao Hirokawa, Aart Middeldorp:
Dependency Pairs Revisited. RTA 2004: 249-268 - 2003
- [j18]Aart Middeldorp:
Preface. Inf. Comput. 183(2): 139 (2003) - [c31]Nao Hirokawa, Aart Middeldorp:
Automating the Dependency Pair Method. CADE 2003: 32-46 - [c30]Nao Hirokawa, Aart Middeldorp:
Tsukuba Termination Tool. RTA 2003: 311-320 - 2002
- [j17]Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema:
Relative Undecidability in Term Rewriting: I. The Termination Hierarchy. Inf. Comput. 178(1): 101-131 (2002) - [j16]Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema:
Relative Undecidability in Term Rewriting: II. The Confluence Hierarchy. Inf. Comput. 178(1): 132-148 (2002) - [j15]Aart Middeldorp, Taro Suzuki, Mohamed Hamada:
Complete Selection Functions for a Lazy Conditional Narrowing Calculus. J. Funct. Log. Program. 2002 (2002) - [c29]