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