Ontology Support for a Lightweight Formal Verification System

The usability of verification systems is becoming increasingly important, and the effective integration of ontologies of formal facts (definitions, propositions, and syntactic idioms) into machine verification systems will likely play a role in improving the usability of such systems. The "aartifact" lightweight verification system utilizes an ontology of formal propositions in order to support lightweight verification of formal arguments that involve common mathematical concepts. The ontology is stored within a relational database, and can be assembled and extended using a simple web interface by contributors who are domain experts. The database can be compiled into two separate components of the "aartifact" system: a verifier component that computes congruence closures of expressions containing relations and predicates found in the ontology, and a JavaScript application that interactively presents to users information about the constants, operators, relations, predicates, syntactic constructs, and idioms found in the ontology (and, thus, supported by the verifier). In this way, the database serves to improve both the verification system's capacity to infer implicit applications of logical propositions within a user's formal argument, and to inform users in a context-aware and structured manner of the verification system's capabilities and limitations