scientific article; zbMATH DE number 3299786
From MaRDI portal
Publication:5581665
zbMath0188.04902MaRDI QIDQ5581665
Publication date: 1970
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (only showing first 100 items - show all)
Conditional term rewriting and first-order theorem proving ⋮ Proving group isomorphism theorems ⋮ A categorical formulation for critical-pair/completion procedures ⋮ Implementing contextual rewriting ⋮ Confluence of terminating membership conditional TRS ⋮ Completeness and confluence of order-sorted term rewriting ⋮ Completion for constrained term rewriting systems ⋮ A proof system for conditional algebraic specifications ⋮ Meta-rule synthesis from crossed rewrite systems ⋮ Completion of first-order clauses with equality by strict superposition ⋮ Completion procedures as semidecision procedures ⋮ Linear completion ⋮ Clausal rewriting ⋮ Design strategies for rewrite rules ⋮ Dynamic temporal logical operations in multi-agent logics ⋮ Unifying splitting ⋮ The Maude strategy language ⋮ Complete equational unification based on an extension of the Knuth-Bendix completion procedure ⋮ Network rewriting utility description ⋮ Shuffle polygraphic resolutions for operads ⋮ Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ An explicit algorithm for normal forms in small overlap monoids ⋮ Positive Plücker tree certificates for non-realizability ⋮ Unnamed Item ⋮ Unification theory ⋮ Automata-driven efficient subterm unification ⋮ On interreduction of semi-complete term rewriting systems ⋮ Decreasing Diagrams and Relative Termination ⋮ Termination Tools in Ordered Completion ⋮ A general framework to build contextual cover set induction provers ⋮ Term rewriting induction ⋮ Ordered rewriting and confluence ⋮ Complete sets of reductions with constraints ⋮ Rewrite systems for varieties of semigroups ⋮ Improving associative path orderings ⋮ On restrictions of ordered paramodulation with simplification ⋮ SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning ⋮ Left-Linear Completion with AC Axioms ⋮ Weighted Path Orders Are Semantic Path Orders ⋮ KBO Constraint Solving Revisited ⋮ Derivation lengths and order types of Knuth--Bendix orders ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ The HOM Problem is EXPTIME-Complete ⋮ High-Level Theories ⋮ Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK ⋮ Rewriting in Gray categories with applications to coherence ⋮ String diagram rewrite theory III: Confluence with and without Frobenius ⋮ Confluence of algebraic rewriting systems ⋮ Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs ⋮ Eta-conversion for the languages of explicit substitutions ⋮ Extending Bachmair's method for proof by consistency to the final algebra ⋮ Some results on the confluence property of combined term rewriting systems ⋮ Automated deduction with associative-commutative operators ⋮ A complete equational axiomatization for prefix iteration ⋮ The shortest single axioms for groups of exponent 4 ⋮ Single identities for ternary Boolean algebras ⋮ Weights for total division orderings on strings ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ Describing symmetrical structures in logic. ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ The Church-Rosser property for ground term-rewriting systems is decidable ⋮ Simplifying conditional term rewriting systems: Unification, termination and confluence ⋮ Embedding Boolean expressions into logic programming ⋮ A class of confluent term rewriting systems and unification ⋮ On deciding the confluence of a finite string-rewriting system on a given congruence class ⋮ History and basic features of the critical-pair/completion procedure ⋮ Automatic inductive theorem proving using Prolog ⋮ Only prime superpositions need be considered in the Knuth-Bendix completion procedure ⋮ Critical pair criteria for completion ⋮ Parallel dynamic semantics of sequential programs with speculative and incremental computation ⋮ Computing a Gröbner basis of a polynomial ideal over a Euclidean domain ⋮ Implementing first-order rewriting with constructor systems ⋮ Pseudo-natural algorithms for finitely generated presentations of monoids and groups ⋮ A multi-level geometric reasoning system for vision ⋮ Finite generation of ambiguity in context-free languages ⋮ A geometrical approach to multiset orderings ⋮ Lifting canonical algorithms from a ring R to the ring R[x] ⋮ Fast Knuth-Bendix completion with a term rewriting system compiler ⋮ Higher-order rewrite systems and their confluence ⋮ Parikh-reducing Church-Rosser representations for some classes of regular languages ⋮ A notation for lambda terms. A generalization of environments ⋮ Knuth's coherent presentations of plactic monoids of type A ⋮ Simple termination of rewrite systems ⋮ A note on simplification orderings ⋮ Undecidable properties of monoids with word problem solvable in linear time. II: Cross sections and homological and homotopical finiteness conditions. ⋮ Undecidable properties of monoids with word problem solvable in linear time. ⋮ A rewriting approach to satisfiability procedures. ⋮ Orienting rewrite rules with the Knuth-Bendix order. ⋮ An upper bound on the derivational complexity of Knuth-Bendix orderings. ⋮ New decision algorithms for finitely presented commutative semigroups ⋮ On using ground joinable equations in equational theorem proving ⋮ Complete positive group presentations. ⋮ A complete proof of correctness of the Knuth-Bendix completion algorithm ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Testing for the Church-Rosser property
This page was built for publication:
