From LCF to Isabelle/HOL.

Lawrence C. Paulson Tobias Nipkow Makarius Wenzel

Published in: Formal Aspects Comput. (2019)

Keyphrases

theorem prover
natural deduction
inference rules
theorem proving
higher order logic
first order logic
sequent calculus
cut elimination
artificial intelligence
reinforcement learning
software engineering
knowledge acquisition
sufficient conditions