scientific article; zbMATH DE number 3870639
From MaRDI portal
Publication:3336735
zbMATH Open0546.68076MaRDI QIDQ3336735FDOQ3336735
Publication date: 1984
Title of this publication is not available (Why is that?)
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)
Cited In (11)
- A superposition oriented theorem prover
- Rewriting with a nondeterministic choice operator
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Building exact computation sequences
- Induction = I-axiomatization + first-order consistency.
- Narrowing vs. SLD-resolution
- Regular substitution sets: A means of controlling E-unification
- 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
Recommendations
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Proofs by induction in equational theories with constructors 👍 👎
- Title not available (Why is that?) 👍 👎
- Higher-order proof construction based on first-order narrowing 👍 👎
- Title not available (Why is that?) 👍 👎
- On the connection between narrowing and proof by consistency 👍 👎
- Title not available (Why is that?) 👍 👎
- Constructor-Based Inductive Theorem Prover 👍 👎
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)
