scientific article; zbMATH DE number 3870639

MaRDI QIDQ3336735zbMATH OpenFDO

Authors Laurent Fribourg

Publication date 1984

zbMATH Keywords

equational clausenarrowingrefutationresolutionsatisfiabilityvalidity

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4060700
• scientific article; zbMATH DE number 4164191
• Proofs by induction in equational theories with constructors
• scientific article; zbMATH DE number 3895059
• Higher-order proof construction based on first-order narrowing
• scientific article; zbMATH DE number 3891336
• On the connection between narrowing and proof by consistency
• scientific article; zbMATH DE number 1302878
• Constructor-Based Inductive Theorem Prover

Cited in

(13)

• A superposition oriented theorem prover
• On solving the equality problem in theories defined by Horn clauses
• Rewriting with a nondeterministic choice operator
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Narrowing vs. SLD-resolution
• A strong restriction of the inductive completion procedure
• Induction = I-axiomatization + first-order consistency.
• scientific article; zbMATH DE number 4164122 (Why is no real title available?)
• Deciding Equality in the Constructor Theory
• scientific article; zbMATH DE number 4060700 (Why is no real title available?)
• Regular substitution sets: A means of controlling E-unification
• On the connection between narrowing and proof by consistency
• Building exact computation sequences

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 Q3336735)