On explicit reflection in theorem proving and formal verification

DOI10.1007/3-540-48660-7_23MaRDI QIDQ4263166zbMATH OpenFDO

Authors Sergei Artemov

Publication date 13 June 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48660-7_23

zbMATH Keywords

reflectionstabilitytheorem provingverification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2185723
• Self-verifying axiom systems, the incompleteness theorem and related reflection principles
• Proof-producing reflection for HOL. With an application to model polymorphism
• scientific article; zbMATH DE number 785045
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)

Cited in

(5)

• Proof-theoretic analysis by iterated reflection
• Proof-producing reflection for HOL. With an application to model polymorphism
• scientific article; zbMATH DE number 2185723 (Why is no real title available?)
• Algebraic Methodology and Software Technology
• Mtac: a monad for typed tactic programming in Coq

This page was built for publication: On explicit reflection in theorem proving and formal verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263166)