scientific article
From MaRDI portal
Publication:3674088
zbMath0523.68080MaRDI QIDQ3674088
Jieh Hsiang, Nachum Dershowitz
Publication date: 1983
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
term rewriting systemsprogram verificationprogramming language designdata type specificationcomplete proof strategies for first order predicate calculusrewrite rules for Boolean algebra
Mechanization of proofs and logical operations (03B35) Data structures (68P05) General topics in the theory of software (68N01)
Related Items
Completion procedures as semidecision procedures, On solving the equality problem in theories defined by Horn clauses, Proof by consistency, An overview of LP, the Larch Prover, Bi-rewriting, a term rewriting technique for monotonic order relations, 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, Unnamed Item, Linear and unit-resulting refutations for Horn theories, Term rewriting and beyond -- theorem proving in Isabelle, Equational completion in order-sorted algebras, Logic and functional programming by retractions, Towards a foundation of completion procedures as semidecision procedures, Discriminator varieties and symbolic computation, Unification in Boolean rings and Abelian groups, Unification in a combination of arbitrary disjoint equational theories, Schematization of infinite sets of rewrite rules generated by divergent completion processes, Boolean unification - the story so far, A categorical critical-pair completion algorithm, A superposition oriented theorem prover, Multi-valued logic and Gröbner bases with applications to modal logic, Equational methods in first order predicate calculus, Semi-unification, Deductive and inductive synthesis of equational programs
