scientific article; zbMATH DE number 3829296
From MaRDI portal
Publication:3674088
zbMATH Open0523.68080MaRDI QIDQ3674088FDOQ3674088
Authors: Jieh Hsiang, Nachum Dershowitz 
Publication date: 1983
Title of this publication is not available (Why is that?)
term rewriting systemsprogram verificationprogramming language designdata type specificationcomplete proof strategies for first order predicate calculusrewrite rules for Boolean algebra
General topics in the theory of software (68N01) Data structures (68P05) Mechanization of proofs and logical operations (03B35)
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
- Completion procedures as semidecision procedures
- Equational methods in first order predicate calculus
- Bi-rewriting, a term rewriting technique for monotonic order relations
- Title not available (Why is that?)
- Semi-unification
- 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)
