A Verified Runtime for a Verified Theorem Prover.

Magnus O. Myreen Jared Davis

Published in: ITP (2011)

Keyphrases

theorem prover
first order logic
term rewriting
data sets
natural deduction
formal proof
feature selection
automated reasoning
higher order logic
artificial intelligence
description logics
graphical models
inference rules
automated theorem proving
mathematical knowledge