SeCaV: A Sequent Calculus Verifier in Isabelle/HOL.

Asta Halkjær From Frederik Krogsdal Jacobsen Jørgen Villadsen

Published in: LSFA (2021)

Keyphrases

natural deduction
sequent calculus
cut elimination
theorem prover
inference rules
theorem proving
linear time temporal logic
proof search
linear logic
artificial intelligence
first order logic
automated reasoning
higher order logic