Using First-Order Theorem Provers in the Jahob Data Structure Verification System.
Charles BouillaguetViktor KuncakThomas WiesKaren ZeeMartin C. RinardPublished in: VMCAI (2007)
Keyphrases
- theorem prover
- first order logic
- data structure
- term rewriting
- formal proof
- theorem proving
- inference rules
- automated theorem proving
- automated reasoning
- automated deduction
- predicate calculus
- propositional logic
- formal semantics
- model checking
- computer algebra
- probabilistic reasoning
- higher order logic
- efficient data structures
- timed automata
- natural deduction
- higher order
- knowledge representation
- proof search
- proof planning
- distributed systems
- horn clauses
- itemsets
- sequent calculus
- high level
- pairwise
- suffix tree
- natural language
- lower layers