pith. sign in

arxiv: 2604.20754 · v1 · submitted 2026-04-22 · 💻 cs.LO

Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version)

Naoki Nishida This is my paper

Pith reviewed 2026-05-09 23:00 UTC · model grok-4.3

classification 💻 cs.LO
keywords term rewrite systemsterminationinnermost terminationdependency pairsoverlay TRSright-linear systemssimulation property
0
0 comments X

The pith

Right-linear overlay term rewrite systems terminate if and only if they innermost terminate.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes an equivalence between termination and innermost termination for right-linear overlay term rewrite systems. It builds on a known simulation property where terminating rewrite sequences can be replicated using only innermost reductions. Using this, the authors prove that the system has no infinite minimal dependency-pair chains exactly when it has no infinite innermost minimal dependency-pair chains. This equivalence means that checking for innermost termination suffices to establish full termination in this class of systems.

Core claim

For a right-linear overlay TRS, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. This implies that a right-linear overlay TRS is terminating if and only if it is innermost terminating.

What carries the argument

The simulation property allowing any terminating rewrite sequence to be simulated by innermost reduction, applied within the dependency pair framework.

If this is right

  • If there is no infinite innermost minimal DP-chain, then there is no infinite minimal DP-chain for right-linear overlay TRSs.
  • Termination of a right-linear overlay TRS is equivalent to its innermost termination.
  • The dependency pair technique can be specialized to innermost chains to prove termination for these systems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This result may simplify automated termination proofs by allowing focus on innermost reductions for overlay systems.
  • It suggests that for classes with similar simulation properties, termination checks can be reduced to innermost ones.
  • Extensions could explore whether similar equivalences hold for non-right-linear or non-overlay TRSs.

Load-bearing premise

The previously established simulation property that any rewrite sequence ending in a normal form in a terminating right-linear overlay TRS can be simulated by innermost reduction.

What would settle it

Finding a right-linear overlay TRS that is innermost terminating but admits an infinite minimal dependency pair chain would disprove the equivalence.

read the original abstract

It has been shown that, regarding a terminating right-linear overlay term rewrite system (TRS), any rewrite sequence ending with a normal form can be simulated by the innermost reduction. In this paper, using this simulation property, we show that for a right-linear overlay TRS, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. This implies that a right-linear overlay TRS is terminating if and only if it is innermost terminating.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper claims that for right-linear overlay term rewrite systems, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. This equivalence is derived from a previously established simulation property (any rewrite sequence to a normal form in a terminating right-linear overlay TRS can be simulated by innermost reduction) and implies that such TRSs are terminating if and only if they are innermost terminating.

Significance. If the central equivalence holds, the result would be a useful addition to the theory of termination for term rewrite systems. It would allow reducing general termination proofs to innermost termination checks for the right-linear overlay class via dependency pairs, potentially simplifying automated analysis. The reliance on the simulation property is a clear methodological strength when the transfer to minimal chains is fully justified.

major comments (2)
  1. [Abstract and proof of the main theorem] Abstract and proof of the main theorem: The simulation property is conditioned on the TRS being terminating, yet it is invoked to establish the equivalence of (non-)existence of infinite minimal DP chains and innermost minimal DP chains. The manuscript must explicitly demonstrate, without presupposing termination, how an infinite innermost minimal chain can be lifted to a standard minimal chain (or vice versa) while preserving minimality conditions; otherwise the argument risks circularity in one direction of the iff.
  2. [Proof of the main theorem] Proof of the main theorem: The abstract indicates that the simulation is used to transfer between standard and innermost DP chains, but provides no details on how the simulation extends to infinite chains or verifies that minimality is preserved under the mapping. This transfer is load-bearing for the central claim and requires a self-contained argument rather than an appeal to the prior result alone.
minor comments (1)
  1. [Abstract] The abstract would be clearer if it briefly indicated the direction in which the simulation is applied and why it does not presuppose the termination result being proved.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need to clarify the proof of the main theorem to avoid any appearance of circularity. We agree that the current presentation relies too heavily on an appeal to the prior simulation result without sufficient detail for the infinite case, and we will revise the manuscript to include a self-contained argument.

read point-by-point responses

  1. Referee: Abstract and proof of the main theorem: The simulation property is conditioned on the TRS being terminating, yet it is invoked to establish the equivalence of (non-)existence of infinite minimal DP chains and innermost minimal DP chains. The manuscript must explicitly demonstrate, without presupposing termination, how an infinite innermost minimal chain can be lifted to a standard minimal chain (or vice versa) while preserving minimality conditions; otherwise the argument risks circularity in one direction of the iff.

    Authors: We accept the point that the current write-up risks suggesting circularity and will revise the proof of the main theorem. The revision will explicitly construct the correspondence for infinite chains by applying the simulation only to finite prefixes of the chain. Because each prefix ends in a minimal term (by the definition of a minimal DP chain), the right-linear overlay properties allow the simulation to be invoked locally on those finite segments without assuming global termination of the TRS. We will prove that the resulting mapped chain remains minimal, thereby establishing both directions of the equivalence directly from the chain definitions. revision: yes

  2. Referee: Proof of the main theorem: The abstract indicates that the simulation is used to transfer between standard and innermost DP chains, but provides no details on how the simulation extends to infinite chains or verifies that minimality is preserved under the mapping. This transfer is load-bearing for the central claim and requires a self-contained argument rather than an appeal to the prior result alone.

    Authors: We agree that the manuscript should not merely cite the prior finite-sequence simulation but must supply the missing details for infinite chains. In the revised version we will insert a dedicated lemma that (i) takes an arbitrary infinite minimal DP chain, (ii) replaces each finite reduction segment between dependency-pair steps by its innermost simulation (justified by right-linearity and the overlay condition on the minimal terms), and (iii) verifies that the image chain is still minimal and infinite. The same construction works in the opposite direction. This lemma will be proved from first principles using only the right-linear overlay assumptions and the definition of minimality, making the argument self-contained. revision: yes

Circularity Check

0 steps flagged

No circularity; central equivalence derived from independent prior simulation result

full rationale

The paper cites a previously established simulation property (any rewrite sequence to a normal form in a terminating right-linear overlay TRS can be simulated by innermost reduction) and uses it to establish the equivalence between absence of infinite minimal DP chains and absence of infinite innermost minimal DP chains. This equivalence then yields termination iff innermost termination. The simulation is an external prior result conditioned on termination, but the paper does not reduce its own claim to a self-definition, a fitted parameter renamed as prediction, or a load-bearing self-citation chain whose validity depends on the present work. No equations or steps in the provided abstract reduce the target statement to its inputs by construction, and the derivation remains self-contained once the cited theorem is granted.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies entirely on standard mathematical concepts from the TRS literature with no additional free parameters, ad-hoc axioms, or invented entities introduced.

axioms (1)
  • standard math Standard definitions and properties of term rewrite systems (TRS), dependency pairs (DP), overlay systems, right-linearity, minimal chains, and innermost reduction.
    These are foundational concepts in the theory of term rewriting systems as used in the abstract.

pith-pipeline@v0.9.0 · 5365 in / 1378 out tokens · 82847 ms · 2026-05-09T23:00:10.560713+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

159 extracted references · 18 canonical work pages

  1. [1]

    2019 , type =

    Yoshiaki Kanazawa and Naoki Nishida and Masahiko Sakai , title =. 2019 , type =

    2019

  2. [2]

    Computer Software , year =

    Naoki Nakabayashi and Naoki Nishida and Keiichirou Kusakari and Toshiki Sakabe and Masahiko Sakai , title =. Computer Software , year =

  3. [3]

    Rewriting Induction for Constrained Term Rewriting Systems , volume =

    Tsubasa Sakata and Naoki Nishida and Toshiki Sakabe and Masahiko Sakai and Keiichirou Kusakari , journal =. Rewriting Induction for Constrained Term Rewriting Systems , volume =

  4. [4]

    Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems , volume =

    Yuki Furuichi and Naoki Nishida and Masahiko Sakai and Keiichirou Kusakari and Toshiki Sakabe , journal =. Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems , volume =

  5. [5]

    Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming , editor =

    Beniamino Accattoli and Bruno Barras , title =. Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming , editor =. 2017 , ourl =. doi:10.1145/3131851.3131855 , publisher =

    work page doi:10.1145/3131851.3131855 2017

  6. [6]

    Proceedings of the 14th International Conference on Formal Aspects of Component Software , pages =

    Kyungmin Bae and Camilo Rocha , title =. Proceedings of the 14th International Conference on Formal Aspects of Component Software , pages =. 2017 , doi =

    2017

  7. [7]

    Programming Languages and Operational Semantics --

    Maribel Fern. Programming Languages and Operational Semantics --. 2014 , ourl =

    2014

  8. [8]

    Proceedings of the 22nd International Conference on Rewriting Techniques and Applications , optbooktitle =

    Stephan Falke and Deepak Kapur and Carsten Sinz , title =. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications , optbooktitle =. 2011 , ourl =. doi:10.4230/LIPIcs.RTA.2011.41 , editor =

    work page doi:10.4230/lipics.rta.2011.41 2011

  9. [9]

    Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation , year =

    Tomohiro Sasano and Naoki Nishida and Masahiko Sakai and Tomoya Ueyama , title =. Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation , year =

  10. [10]

    Automated termination analysis of

    Carsten Otto and Marc Brockschmidt and Christian von Essen and J. Automated termination analysis of. Proceedings of the 21st International Conference on Rewriting Techniques and Applications , optbooktitle =. 2010 , doi =

    2010

  11. [11]

    Automated Induction with Constrained Tree Automata , volume =

    Adel Bouhoula and Florent Jacquemard , booktitle =. Automated Induction with Constrained Tree Automata , volume =. doi:10.1007/978-3-540-71070-7_44 , editor =

    work page doi:10.1007/978-3-540-71070-7_44

  12. [12]

    Bradley and Zohar Manna , doi =

    Aaron R. Bradley and Zohar Manna , doi =. The Calculus of Computation: Decision Procedures with Applications to Verification , year =

  13. [13]

    Term Rewriting and All That , year =

    Franz Baader and Tobias Nipkow , doi =. Term Rewriting and All That , year =

  14. [14]

    2018 , doi =

    A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems , booktitle =. 2018 , doi =

    2018

  15. [15]

    Proving Termination of Integer Term Rewriting , volume =

    Carsten Fuhs and J. Proving Termination of Integer Term Rewriting , volume =. Proceedings of the 20th International Conference on Rewriting Techniques and Applications , doi =

  16. [16]

    Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures , volume =

    Stephan Falke and Deepak Kapur , booktitle =. Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures , volume =. doi:10.1007/978-3-540-70590-1_7 , editor =

    work page doi:10.1007/978-3-540-70590-1_7

  17. [17]

    A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs , volume =

    Stephan Falke and Deepak Kapur , booktitle =. A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs , volume =. doi:10.1007/978-3-642-02959-2_22 , editor =

    work page doi:10.1007/978-3-642-02959-2_22

  18. [18]

    Rewriting Induction + Linear Arithmetic = Decision Procedure , volume =

    Stephan Falke and Deepak Kapur , booktitle =. Rewriting Induction + Linear Arithmetic = Decision Procedure , volume =. doi:10.1007/978-3-642-31365-3_20 , editor =

    work page doi:10.1007/978-3-642-31365-3_20

  19. [19]

    Verifying Procedural Programs via Constrained Rewriting Induction , volume =

    Carsten Fuhs and Cynthia Kop and Naoki Nishida , doi =. Verifying Procedural Programs via Constrained Rewriting Induction , volume =. ACM Transactions on Computational Logic , optjournal =

  20. [20]

    The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs , fullbooktitle =

    J. The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs , fullbooktitle =. Proc.\ LPAR 2004 , pages =. 2004 , doi =

    2004

  21. [21]

    Proof by Induction in Equational Theories with Constructors , volume =

    G\'erard Huet and Jean-Marie Hullot , doi =. Proof by Induction in Equational Theories with Constructors , volume =. Journal of Computer and System Science , number =

  22. [22]

    Term Rewriting with Logical Constraints , volume =

    Cynthia Kop and Naoki Nishida , booktitle =. Term Rewriting with Logical Constraints , volume =. doi:10.1007/978-3-642-40885-4_24 , editor =

    work page doi:10.1007/978-3-642-40885-4_24

  23. [23]

    Proceedings of the 13th International Workshop on Termination , pages =

    Cynthia Kop , title =. Proceedings of the 13th International Workshop on Termination , pages =

  24. [24]

    Automatic Constrained Rewriting Induction towards Verifying Procedural Programs , volume =

    Cynthia Kop and Naoki Nishida , booktitle =. Automatic Constrained Rewriting Induction towards Verifying Procedural Programs , volume =. doi:10.1007/978-3-319-12736-1_18 , editor =

    work page doi:10.1007/978-3-319-12736-1_18

  25. [25]

    doi:10.1007/978-3-662-48899-7_38 , editor =

    Cynthia Kop and Naoki Nishida , booktitle =. doi:10.1007/978-3-662-48899-7_38 , editor =

    work page doi:10.1007/978-3-662-48899-7_38

  26. [26]

    Musser , booktitle =

    David R. Musser , booktitle =. On Proving Inductive Properties of Abstract Data Types , year =. doi:10.1145/567446.567461 , editor =

    work page doi:10.1145/567446.567461

  27. [27]

    On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants , year =

    Naoki Nishida and Takumi Kataoka , booktitle =. On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants , year =

  28. [28]

    Science of Computer Programming , volume =

    Takahiro Nagao and Naoki Nishida , title =. Science of Computer Programming , volume =. 2018 , xmonth = apr, doi =

    2018

  29. [29]

    Advanced Topics in Term Rewriting , year =

    Enno Ohlebusch , doi =. Advanced Topics in Term Rewriting , year =

  30. [30]

    Reddy , fullbooktitle =

    Uday S. Reddy , fullbooktitle =. Term Rewriting Induction , volume =. Proc.\ CADE 1990 , series =. doi:10.1007/3-540-52885-7_86 , xeditor =

    work page doi:10.1007/3-540-52885-7_86 1990

  31. [31]

    Reynolds , doi =

    John C. Reynolds , doi =. Theories of Programming Languages , year =

  32. [32]

    On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs , volume =

    Tsubasa Sakata and Naoki Nishida and Toshiki Sakabe , booktitle =. On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs , volume =. doi:10.1007/978-3-642-22531-4_9 , editor =

    work page doi:10.1007/978-3-642-22531-4_9

  33. [33]

    Closed Symbolic Execution for Verifying Program Termination , year =

    Germ. Closed Symbolic Execution for Verifying Program Termination , year =. Proceedings of the 12th. doi:10.1109/SCAM.2012.13 , optbooktitle =

    work page doi:10.1109/scam.2012.13 2012

  34. [34]

    Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction , optbooktitle =

    Sarah Winkler and Aart Middeldorp , title =. Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction , optbooktitle =. 2018 , editor =

    2018

  35. [35]

    Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments , optbooktitle =

    Naoki Nishida and Sarah Winkler , title =. Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments , optbooktitle =. 2018 , editor =

    2018

  36. [36]

    Reachability Analysis of Term Rewriting Systems with

    Thomas Genet and Val. Reachability Analysis of Term Rewriting Systems with. Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning , optbooktitle =. 2001 , editor =

    2001

  37. [37]

    Tanenbaum and Albert S

    Andrew S. Tanenbaum and Albert S. Woodhull , title =

  38. [38]

    Decision Procedures: An Algorithmic Point of View , year =

    Daniel Kroening and Ofer Strichman , Date-Added =. Decision Procedures: An Algorithmic Point of View , year =

  39. [39]

    Verma , title =

    Guillem Godoy and Ashish Tiwari and Rakesh M. Verma , title =. Proceedings of the 20th Annual Symposium on Theoretical Aspects of Computer Science , pages =. 2003 , editor =

    2003

  40. [40]

    Proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation , optbooktitle =

    Yoshiaki Kanazawa and Naoki Nishida , title =. Proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation , optbooktitle =. 2019 , series =

    2019

  41. [41]

    Donald Ervin Knuth , title =

  42. [42]

    K Overview and

    Grigore Ro. K Overview and. Proceedings of the Second International Workshop on the. 2014 , doi =

    2014

  43. [43]

    All-Path Reachability Logic , optjournal =

    Andrei. All-Path Reachability Logic , optjournal =. Logical Methods in Computer Science , volume =. 2019 , doi =

    2019

  44. [44]

    All-Path Reachability Logic , booktitle =

    Andrei. All-Path Reachability Logic , booktitle =. 2014 , doi =

    2014

  45. [45]

    Tanenbaum , title =

    Andrew S. Tanenbaum , title =

  46. [46]

    Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics , editor =

    Andrei-Sebastian Buruian. Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics , editor =. Proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation , optbooktitle =. doi:10.4204/EPTCS.289.1 , year =

    work page doi:10.4204/eptcs.289.1

  47. [47]

    Allen Emerson and Joseph Y

    E. Allen Emerson and Joseph Y. Halpern , title =. Conference Record of the Tenth Annual. 1983 , doi =

    1983

  48. [48]

    Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , optbooktitle =

    James Brotherston , title =. Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , optbooktitle =. 2005 , doi =

    2005

  49. [49]

    Principles of model checking , publisher =

    Christel Baier and Joost. Principles of model checking , publisher =

  50. [50]

    Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , optbooktitle =

    Leonardo Mendon. Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , optbooktitle =. 2008 , doi =

    2008

  51. [51]

    Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability , booktitle =

    Toshinori Takai and Yuichi Kaji and Hiroyuki Seki , editor =. Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability , booktitle =. 2000 , doi =

    2000

  52. [52]

    Journal of Symbolic Computation , optjournal =

    Thomas Genet and Vlad Rusu , title =. Journal of Symbolic Computation , optjournal =. 2010 , doi =

    2010

  53. [53]

    Decidable Approximations of Term Rewriting Systems , booktitle =

    Florent Jacquemard , editor =. Decidable Approximations of Term Rewriting Systems , booktitle =. 1996 , doi =

    1996

  54. [54]

    Proceedings of the 30th International Conference on Computer Aided Verification , optbooktitle =

    Grigory Fedyukovich and Yueling Zhang and Aarti Gupta , title =. Proceedings of the 30th International Conference on Computer Aided Verification , optbooktitle =. 2018 , doi =

    2018

  55. [55]

    Proceedings of the 26th International Symposium on Static Analysis , optbooktitle =

    Naoki Kobayashi and Takeshi Nishikawa and Atsushi Igarashi and Hiroshi Unno , title =. Proceedings of the 26th International Symposium on Static Analysis , optbooktitle =. 2019 , doi =

    2019

  56. [56]

    An overview of the

    Grigore Ro. An overview of the. Journal of Logic and Algebraic Programming , volume =. 2010 , doi =

    2010

  57. [57]

    Proceedings of the ACM on Programming Languages , volume =

    Takeshi Tsukada and Hiroshi Unno , title =. Proceedings of the ACM on Programming Languages , volume =. 2022 , doi =

    2022

  58. [58]

    Peterson , title =

    Gary L. Peterson , title =. Information Processing Letters , optjournal =. 1981 , doi =

    1981

  59. [59]

    Proceedings of the 18th International Conference on Evaluation of Novel Approaches to Software Engineering , optbooktitle =

    Hiromasa Ito and Yutaka Matsubara and Hiroaki Takada , title =. Proceedings of the 18th International Conference on Evaluation of Novel Approaches to Software Engineering , optbooktitle =. 2023 , pages =

    2023

  60. [60]

    Model checking linear temporal logic of rewriting formulas under localized fairness , journal =

    Kyungmin Bae and Jos. Model checking linear temporal logic of rewriting formulas under localized fairness , journal =. 2015 , doi =

    2015

  61. [61]

    Abstract Logical Model Checking of Infinite-State Systems Using Narrowing , booktitle =

    Kyungmin Bae and Santiago Escobar and Jos. Abstract Logical Model Checking of Infinite-State Systems Using Narrowing , booktitle =. 2013 , doi =

    2013

  62. [62]

    Donaldson and Adam Betts , title =

    Paul Thomson and Alastair F. Donaldson and Adam Betts , title =. ACM Transactions on Parallel Computing , optjournal =. 2016 , doi =

    2016

  63. [63]

    Miller and Lars Fredriksen and Bryan So , title =

    Barton P. Miller and Lars Fredriksen and Bryan So , title =. Communications of the ACM , optjournal =. 1990 , doi =

    1990

  64. [64]

    Concurrent Software Quality , optjournal =

    Haojie Fu and Zan Wang and Xiang Chen and Xiangyu Fan , title =. Concurrent Software Quality , optjournal =. 2018 , doi =

    2018

  65. [65]

    Alshmrany and Mohannad Aldughaim and Ahmed Bhayat and Lucas C

    Kaled M. Alshmrany and Mohannad Aldughaim and Ahmed Bhayat and Lucas C. Cordeiro , editor =. Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering , optbooktitle =. 2022 , doi =

    2022

  66. [66]

    A Survey of Recent Trends in Testing Concurrent Software Systems , journal =

    Francesco Adalberto Bianchi and Alessandro Margara and Mauro Pezz. A Survey of Recent Trends in Testing Concurrent Software Systems , journal =. 2018 , doi =

    2018

  67. [67]

    Canonical Forms and Unification , booktitle =

    Jean. Canonical Forms and Unification , booktitle =. 1980 , doi =

    1980

  68. [68]

    Hubert Comon and Max Dauchet and R\'emi Gilleron and Florent Jacquemard and Denis Lugiez and Christof L\"oding and Sophie Tison and Marc Tommasi , title =

  69. [69]

    Logical Methods in Computer Science , optjournal =

    Naoki Nishida and Masahiko Sakai and Toshiki Sakabe , title =. Logical Methods in Computer Science , optjournal =. 2012 , volume =

    2012

  70. [70]

    Allen , editor =

    Frances E. Allen , editor =. Control flow analysis , booktitle =. 1970 , doi =

    1970

  71. [71]

    Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems , optbooktitle =

    Marc Brockschmidt and Byron Cook and Samin Ishtiaq and Heidy Khlaaf and Nir Piterman , editor =. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems , optbooktitle =. 2016 , doi =

    2016

  72. [72]

    2021 , xaddress =

    Donghoon Shin , title =. 2021 , xaddress =

    2021

  73. [73]

    Journal of Symbolic Computation , optjournal =

    Nachum Dershowitz , title =. Journal of Symbolic Computation , optjournal =. 1987 , doi =

    1987

  74. [74]

    2016 , doi =

    Daniel Kroening and Ofer Strichman , title =. 2016 , doi =

    2016

  75. [75]

    2018 , xeprinttype =

    A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems , journal =. 2018 , xeprinttype =

    2018

  76. [76]

    2015 , type =

    Tomoya Ueyama and Naoki Nishida and Masahiko Sakai and Toshiki Sakabe , title =. 2015 , type =

    2015

  77. [77]

    Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming , optbooktitle =

    Naoki Nishida and Masahiko Sakai and Toshiki Sakabe , title =. Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming , optbooktitle =. 2003 , editor =

    2003

  78. [78]

    Journal of Logical and Algebraic Methods in Programming , optjournal =

    Operationally-based program equivalence proofs using. Journal of Logical and Algebraic Methods in Programming , optjournal =. 2023 , xmonth = oct, xurl =

    2023

  79. [79]

    Computer Software , volume=

    Decision Method of Reachability based on Rewrite Rule Overlapping , author=. Computer Software , volume=. 2016 , doi=

    2016

  80. [80]

    Information and Computation , optjournal =

    Takashi Nagaya and Yoshihito Toyama , title =. Information and Computation , optjournal =. 2002 , doi =

    2002

Showing first 80 references.