Using Isabelle/HOL to Verify First-Order Relativity Theory.

Mike Stannett István Németi

Published in: J. Autom. Reason. (2014)

Keyphrases

theorem prover
first order logic
natural deduction
theoretical framework
formal methods
term rewriting
theorem proving
theoretical basis
data sets
higher order
inference rules
logical theories
information systems
knowledge representation
theoretical foundation
quantifier free