Show simple item record

dc.contributor.authorLapets, Andreien_US
dc.contributor.authorLalwani, Prakashen_US
dc.contributor.authorKfoury, Assafen_US
dc.date.accessioned2012-05-21T18:59:35Z
dc.date.available2012-05-21T18:59:35Z
dc.date.issued2010-05-14
dc.identifier.citationLapets, Andrei; Lalwani, Prakash; Kfoury, Assaf. "Ontology Support for a Lightweight Formal Verification System", Technical Report BUCS-TR-2010-012, Computer Science Department, Boston University, May 14, 2010. [Available from: http://hdl.handle.net/2144/3791]
dc.identifier.urihttps://hdl.handle.net/2144/3791
dc.description.abstractThe 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.en_US
dc.language.isoen_US
dc.publisherCS Department, Boston Universityen_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2010-012
dc.titleOntology Support for a Lightweight Formal Verification Systemen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record