Certified Connection Tableaux Proofs for HOL Light and TPTP.
Cezary KaliszykJosef UrbanJirí VyskocilPublished in: CPP (2015)
Keyphrases
- theorem prover
- automated theorem proving
- theorem proving
- natural deduction
- decision procedures
- automated reasoning
- first order logic
- proof procedure
- inference rules
- modal logic
- formal proof
- computer algebra
- mathematical proofs
- higher order logic
- cut elimination
- integrity constraints
- databases
- computer programs
- functional dependencies
- sequent calculus
- proof search
- higher order
- data structure