scientific article; zbMATH DE number 3829296
From MaRDI portal
Publication:3674088
Cited in
(27)- On solving the equality problem in theories defined by Horn clauses
- Boolean unification - the story so far
- Multi-valued logic and Gröbner bases with applications to modal logic
- Equational methods in first order predicate calculus
- Deductive and inductive synthesis of equational programs
- Equational completion in order-sorted algebras
- scientific article; zbMATH DE number 3860380 (Why is no real title available?)
- Schematization of infinite sets of rewrite rules generated by divergent completion processes
- Discriminator varieties and symbolic computation
- An overview of LP, the Larch Prover
- Term rewriting and beyond -- theorem proving in Isabelle
- Unification in Boolean rings
- Semi-unification
- A categorical critical-pair completion algorithm
- History and basic features of the critical-pair/completion procedure
- Logic and functional programming by retractions
- Rewrite method for theorem proving in first order theory with equality
- Linear and unit-resulting refutations for Horn theories
- Unification in combinations of collapse-free regular theories
- Proof by consistency
- Bi-rewriting, a term rewriting technique for monotonic order relations
- Completion procedures as semidecision procedures
- Termination of rewriting
- Towards a foundation of completion procedures as semidecision procedures
- A superposition oriented theorem prover
- Unification in Boolean rings and Abelian groups
- Unification in a combination of arbitrary disjoint equational theories
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3674088)
