scientific article; zbMATH DE number 3870639
From MaRDI portal
Publication:3336735
zbMATH Open0546.68076MaRDI QIDQ3336735FDOQ3336735
Authors: Laurent Fribourg 
Publication date: 1984
Title of this publication is not available (Why is that?)
Recommendations
- scientific article; zbMATH DE number 4060700
- scientific article
- 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
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)
Cited In (13)
- A superposition oriented theorem prover
- Rewriting with a nondeterministic choice operator
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Building exact computation sequences
- Deciding Equality in the Constructor Theory
- Induction = I-axiomatization + first-order consistency.
- Narrowing vs. SLD-resolution
- Regular substitution sets: A means of controlling E-unification
- Title not available (Why is that?)
- On the connection between narrowing and proof by consistency
- Title not available (Why is that?)
- A strong restriction of the inductive completion procedure
- 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 Q3336735)
