scientific article

zbMath0546.68076MaRDI QIDQ3336735

Laurent Fribourg

Publication date: 1984

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

validityresolutionsatisfiabilitynarrowingrefutationequational clause

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Related Items (9)

On solving the equality problem in theories defined by Horn clauses ⋮ Regular substitution sets: A means of controlling E-unification ⋮ Rewriting with a nondeterministic choice operator ⋮ Simplifying conditional term rewriting systems: Unification, termination and confluence ⋮ Narrowing vs. SLD-resolution ⋮ Building exact computation sequences ⋮ A strong restriction of the inductive completion procedure ⋮ Induction = I-axiomatization + first-order consistency. ⋮ A superposition oriented theorem prover

This page was built for publication: