scientific article; zbMATH DE number 88983

MaRDI QIDQ4016540zbMATH OpenFDO

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

Publication date 16 January 1993

zbMATH Keywords

associativity of APPEND without inductionderived rule of inferenceinstantiation of function symbols

Mathematics Subject Classification ID

Logic programming (68N17)

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

Cited in

(19)

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

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)