Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant.
Hans-Jörg SchurrMathias FleuryMartin DesharnaisPublished in: SMT (2021)
Keyphrases
- fine grained
- theorem prover
- mathematical proofs
- theorem proving
- coarse grained
- interactive theorem proving
- automated theorem provers
- natural deduction
- formal proof
- proof search
- test bed
- sequent calculus
- automated theorem proving
- access control
- tightly coupled
- cut elimination
- high level
- computer algebra
- decision procedures
- massively parallel
- mathematical knowledge
- image reconstruction
- first order logic