scientific article

zbMath0755.68120MaRDI QIDQ4016540

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

Publication date: 16 January 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

associativity of APPEND without inductionderived rule of inferenceinstantiation of function symbols

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items

On definitions of constants and types in HOL ⋮ A mechanically verified incremental garbage collector ⋮ Theory extension in ACL2(r) ⋮ Rewriting with equivalence relations in ACL2 ⋮ A mechanical analysis of program verification strategies ⋮ An ACL2 Tutorial ⋮ An extension of the Boyer-Moore theorem prover to support first-order quantification ⋮ A verification system for concurrent programs based on the Boyer-Moore prover ⋮ Machine checked proofs of the design of a fault-tolerant circuit ⋮ Second-Order Programs with Preconditions ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Integrating external deduction tools with ACL2 ⋮ Limited second-order functionality in a first-order setting ⋮ Specification and verification of concurrent programs through refinements