Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving.
Michael J. C. GordonJoe HurdKonrad SlindPublished in: CHARME (2003)
Keyphrases
- formal semantics
- theorem proving
- specification language
- first order logic
- theorem prover
- formal specification
- automated reasoning
- programming language
- description language
- inference rules
- decision procedures
- propositional logic
- proof planning
- knowledge representation
- operational semantics
- parallel search
- geometry theorem proving
- machine learning
- consequence finding
- owl dl ontology
- databases