Tyrolean

swMATH7830MaRDI QIDQ19846

No author found.

Related Items (92)

Relative termination via dependency pairs ⋮ A combination framework for complexity ⋮ A Tool Proving Well-Definedness of Streams Using Termination Tools ⋮ Dynamic Dependency Pairs for Algebraic Functional Systems ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Generalized and Formalized Uncurrying ⋮ Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ KBO orientability ⋮ KBCV – Knuth-Bendix Completion Visualizer ⋮ Certification of Termination Proofs Using CeTA ⋮ Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Multi-completion with termination tools ⋮ Uncurrying for termination and complexity ⋮ Termination of Cycle Rewriting by Transformation and Matrix Interpretation ⋮ Satisfiability Checking: Theory and Applications ⋮ Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems ⋮ Tyrolean termination tool: techniques and features ⋮ On tree automata that certify termination of left-linear term rewriting systems ⋮ Mechanizing and improving dependency pairs ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Decreasing diagrams and relative termination ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Usable Rules for Context-Sensitive Rewrite Systems ⋮ Proving Termination Using Recursive Path Orders and SAT Solving ⋮ Checking Conservativity of Overloaded Definitions in Higher-Order Logic ⋮ Unnamed Item ⋮ Termination of just/fair computations in term rewriting ⋮ KBOs, ordinals, subrecursive hierarchies and all that ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ Matrix interpretations for proving termination of term rewriting ⋮ Automated Complexity Analysis Based on the Dependency Pair Method ⋮ Derivational Complexity of Knuth-Bendix Orders Revisited ⋮ Certifying a Termination Criterion Based on Graphs, without Graphs ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ Term Rewriting and Applications ⋮ Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Attack-defense trees ⋮ Modular Complexity Analysis for Term Rewriting ⋮ Reachability, confluence, and termination analysis with state-compatible automata ⋮ Frontiers of Combining Systems ⋮ The recursive path and polynomial ordering for first-order and higher-order terms ⋮ AC Dependency Pairs Revisited ⋮ A Transformational Approach to Prove Outermost Termination Automatically ⋮ Monotonicity Criteria for Polynomial Interpretations over the Naturals ⋮ Proving operational termination of membership equational programs ⋮ From Outermost Termination to Innermost Termination ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Beyond Dependency Graphs ⋮ On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting ⋮ Context-sensitive dependency pairs ⋮ Predictive Labeling with Dependency Pairs Using SAT ⋮ Dependency Pairs for Rewriting with Non-free Constructors ⋮ Certification of Proving Termination of Term Rewriting by Matrix Interpretations ⋮ AC Completion with Termination Tools ⋮ CSI – A Confluence Tool ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ SAT Solving for Termination Analysis with Polynomial Interpretations ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ The Derivational Complexity Induced by the Dependency Pair Method ⋮ Using well-founded relations for proving operational termination ⋮ Nominal Confluence Tool ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ Loops under Strategies ⋮ Proving Termination of Integer Term Rewriting ⋮ Well-Definedness of Streams by Termination ⋮ The Derivational Complexity Induced by the Dependency Pair Method ⋮ Unnamed Item ⋮ Argument Filterings and Usable Rules for Simply Typed Dependency Pairs ⋮ Match-bounds revisited ⋮ Increasing interpretations ⋮ Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering ⋮ Proving Termination with (Boolean) Satisfaction ⋮ SGGS decision procedures ⋮ Tuple interpretations for termination of term rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ Modular Complexity Analysis via Relative Complexity ⋮ CERTIFIED SUBTERM CRITERION AND CERTIFIED USABLE RULES ⋮ Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity ⋮ Proving Termination of Context-Sensitive Rewriting with MU-TERM ⋮ Innermost Termination of Rewrite Systems by Labeling ⋮ Pattern eliminating transformations

This page was built for software: Tyrolean