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