Extending a Brainiac Prover to Lambda-Free Higher-Order Logic.

Petar Vukmirovic Jasmin Christian Blanchette Simon Cruanes Stephan Schulz

Published in: TACAS (1) (2019)

Keyphrases

higher order logic
theorem prover
higher order
theorem proving
first order logic
automated theorem proving
conditional logic
automated reasoning
inference rules
fixed point
pairwise
model checking
logical framework