scientific article; zbMATH DE number 88983

zbMATH Open0755.68120MaRDI QIDQ4016540FDOQ4016540

Authors: Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J Strother Moore 

Publication date: 16 January 1993

Title of this publication is not available (Why is that?)

Recommendations

• A theorem prover for a computational logic
• Partial instantiation methods for inference in first-order logic
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Proving and rewriting
• Limited second-order functionality in a first-order setting

zbMATH Keywords

associativity of APPEND without inductionderived rule of inferenceinstantiation of function symbols

Mathematics Subject Classification ID

Logic programming (68N17)

Cited In (18)

• An extension of the Boyer-Moore theorem prover to support first-order quantification
• Specification and verification of concurrent programs through refinements
• A macro for reusing abstract functions and theorems
• On definitions of constants and types in HOL
• A theorem prover for a computational logic
• A verification system for concurrent programs based on the Boyer-Moore prover
• Rewriting with equivalence relations in ACL2
• Integrating external deduction tools with ACL2
• Partial instantiation methods for inference in first-order logic
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Limited second-order functionality in a first-order setting
• Theory extension in ACL2(r)
• First-order functional languages and intensional logic
• A mechanically verified incremental garbage collector
• Second-order programs with preconditions
• An ACL2 Tutorial
• A mechanical analysis of program verification strategies
• Machine checked proofs of the design of a fault-tolerant circuit

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