Term Rewriting and All That
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Labelled splitting
- Inductive proof search modulo
- The lambda-context calculus (extended version)
- Increasing interpretations
- Systems of reductions
- Rewriting techniques and applications. 3rd international conference, RTA-89, Chapel Hill, NC, USA, April 3--5, 1989. Proceedings
- Deciding the word problem in the union of equational theories.
- Decidability for left-linear growing term rewriting systems.
- Theorem proving modulo
- Equational rules for rewriting logic
- Loop detection by logically constrained term rewriting
- Crystal monoids \& crystal bases: rewriting systems and biautomatic structures for plactic monoids of types \(A_{n}\), \(B_{n}\), \(C_{n}\), \(D_{n}\), and \(G_{2}\)
- Geometric and combinatorial views on asynchronous computability
- Introduction to ``Milestones in interactive theorem proving
- Formalization of the resolution calculus for first-order logic
- Rewriting systems over similarity and generalized pseudometric spaces and their properties
- Linguistic\(\leftrightarrow \)rational agents' semantics
- Transparent rule based CAS to support formalization of knowledge
- From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
- Taylor term does not imply any nontrivial linear one-equality Maltsev condition
- Confluence and convergence modulo equivalence in probabilistically terminating reduction systems
- Conditional congruence closure over uninterpreted and interpreted symbols
- Intensional computation with higher-order functions
- Modeling dynamic programming problems over sequences and trees with inverse coupled rewrite systems
- Combalgebraic structures on decorated cliques
- Free operated monoids and rewriting systems
- Constraint solving for proof planning
- A theory of reversibility for Erlang
- Constant runtime complexity of term rewriting is semi-decidable
- Relative undecidability in term rewriting. I: The termination hierarchy
- Relative undecidability in term rewriting. II: The confluence hierarchy
- Context-sensitive rewriting strategies
- Some general results about proof normalization
- On rewriting rules in Mizar
- Superposition decides the first-order logic fragment over ground theories
- Colored operads, series on colored operads, and combinatorial generating systems
- Verifying polymer reaction networks using bisimulation
- A superposition calculus for abductive reasoning
- On finite complete rewriting systems, finite derivation type, and automaticity for homogeneous monoids
- Termination of the F5 algorithm
- Duality of graded graphs through operads
- A logic based approach to finding real singularities of implicit ordinary differential equations
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Equational theorem proving modulo
- Multi-dimensional interpretations for termination of term rewriting
- An automated approach to the Collatz conjecture
- Derivational complexity and context-sensitive Rewriting
- A local characterization of B₂ regular crystals
- Fast and parallel decomposition of constraint satisfaction problems
- Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
- Deciding the word problem for ground identities with commutative and extensional symbols
- Tuple interpretations for termination of term rewriting
- Fast left Kan extensions using the chase
- Ground joinability and connectedness in the superposition calculus
- Term orderings for non-reachability of (conditional) rewriting
- A framework for approximate generalization in quantitative theories
- From Hertzsprung's problem to pattern-rewriting systems
- Runtime complexity analysis of logically constrained rewriting
- Pattern eliminating transformations
- Terminating non-disjoint combined unification
- A proof method for local sufficient completeness of term rewriting systems
- MetaFEM: a generic FEM solver by meta-expressions
- Towards finding longer proofs
- AC simplifications and closure redundancies in the superposition calculus
- Moving the bar on computationally sound exclusive-or
- Analogical proportions
- Hopf algebra of multidecorated rooted forests, free matching Rota-Baxter algebras and Gröbner-Shirshov bases
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- Commutative rational term rewriting
- The spirit of node replication
- Certifying proofs in the first-order theory of rewriting
- Parallel coherent graph transformations
- Convergent presentations and polygraphic resolutions of associative algebras
- Compilation of static and evolving conditional knowledge bases for computing induced nonmonotonic inference relations
- Topological rewriting systems applied to standard bases and syntactic algebras
- Unification modulo lists with reverse relation with certain word equations
- Restricted combinatory unification
- Model completeness, covers and superposition
- Confluence by critical pair analysis revisited
- Composing proof terms
- Certified equational reasoning via ordered completion
- The number of clones determined by disjunctions of unary relations
- Set-blocked clause and extended set-blocked clause in first-order logic
- Inductive theorem proving based on tree grammars
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- Non-linear rewrite closure and weak normalization
- Emptiness and finiteness for tree automata with global reflexive disequality constraints
- Labelings for decreasing diagrams
- Relative termination via dependency pairs
- Confluence of orthogonal term rewriting systems in the prototype verification system
- Extended feature algebra
- SAT solving for termination proofs with recursive path orders and dependency pairs
- On explicit substitution with names
- Lower bounds for runtime complexity of term rewriting
- Reduction operators and completion of rewriting systems
- Resolution with order and selection for hybrid logics
- A graphical user interface for formal proofs in geometry
- Reasoning in description logics by a reduction to disjunctive datalog
- Confluence theory for graphs
- Expression reduction systems with patterns
This page was built for publication: Term Rewriting and All That
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4702972)
