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)

• An extension of the Boyer-Moore theorem prover to support first-order quantification
• Specification and verification of concurrent programs through refinements
• On definitions of constants and types in HOL
• A macro for reusing abstract functions and theorems
• Second-order functions and theorems in ACL2
• A verification system for concurrent programs based on the Boyer-Moore prover
• A theorem prover for a computational logic
• 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)