Tyrolean
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Proving Termination of Integer Term Rewriting
- The recursive path and polynomial ordering for first-order and higher-order terms
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
- A tool proving well-definedness of streams using termination tools
- Predictive Labeling with Dependency Pairs Using SAT
- Mechanizing and improving dependency pairs
- Tyrolean termination tool: techniques and features
- Matrix interpretations for proving termination of term rewriting
- On tree automata that certify termination of left-linear term rewriting systems
- Context-sensitive dependency pairs
- Dynamic dependency pairs for algebraic functional systems
- NaTT
- Usable Rules for Context-Sensitive Rewrite Systems
- Proving Termination with (Boolean) Satisfaction
- Automated Complexity Analysis Based on the Dependency Pair Method
- Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
- Termination of just/fair computations in term rewriting
- From Outermost Termination to Innermost Termination
- KBCV – Knuth-Bendix Completion Visualizer
- Well-Definedness of Streams by Termination
- Termination of Isabelle functions via termination of rewriting
- Reachability, confluence, and termination analysis with state-compatible automata
- Termination proofs in the dependency pair framework May induce multiple recursive derivational complexity
- Certified subterm criterion and certified usable rules
- Loop detection in term rewriting using the eliminating unfoldings
- Monotonicity criteria for polynomial interpretations over the naturals
- Proving Termination Using Recursive Path Orders and SAT Solving
- Innermost termination of rewrite systems by labeling
- Term Rewriting and Applications
- SGGS decision procedures
- SAT Solving for Termination Analysis with Polynomial Interpretations
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- Generalized and formalized uncurrying
- AC completion with termination tools
- On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
- Modular complexity analysis for term rewriting
- Match-bounds revisited
- Tuple interpretations for termination of term rewriting
- Multi-dimensional interpretations for termination of term rewriting
- Nominal confluence tool
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- A combination framework for complexity
- Proving operational termination of membership equational programs
- Harnessing first order termination provers using higher order dependency pairs
- Term orderings for non-reachability of (conditional) rewriting
- A Transformational Approach to Prove Outermost Termination Automatically
- Uncurrying for termination and complexity
- Pattern eliminating transformations
- Proving termination of context-sensitive rewriting with MU-TERM
- Using well-founded relations for proving operational termination
- Loops under Strategies
- CSI -- a confluence tool
- Certification of Termination Proofs Using CeTA
- Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
- Polynomial interpretations over the natural, rational and real numbers revisited
- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
- Reducing relative termination to dependency pair problems
- The Derivational Complexity Induced by the Dependency Pair Method
- Beyond Dependency Graphs
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Frontiers of Combining Systems
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
- Decreasing diagrams and relative termination
- Proving termination by dependency pairs and inductive theorem proving
- Polynomials over the reals in proofs of termination : from theory to practice
- Proving termination of context-sensitive rewriting by transformation
- Disproving confluence of term rewriting systems by interpretation and ordering
- Argument filterings and usable rules for simply typed dependency pairs
- Termination of cycle rewriting by transformation and matrix interpretation
- Certifying a Termination Criterion Based on Graphs, without Graphs
- Derivational Complexity of Knuth-Bendix Orders Revisited
- Relative termination via dependency pairs
- KBO orientability
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Modular complexity analysis via relative complexity
- Dependency Pairs for Rewriting with Non-free Constructors
- The derivational complexity induced by the dependency pair method
- Attack-defense trees
- TALP
- CLEAN
- Haskell
- OBJ3
- CeTA
- Timbuk
- SPIKE
- AProVE
- CSI
- CoLoR
- MTT
- CiME
- mkbTT
- Jambox
- MU-TERM
- IsaFoR
- Matchbox
- Slothrop
- Saigawa
This page was built for software: Tyrolean
