Show simple item record

dc.contributor.authorAameri, Bahar
dc.date.accessioned2011-03-08T16:55:24Z
dc.date.available2011-03-08T16:55:24Z
dc.date.issued2011-03-08
dc.identifier.urihttp://hdl.handle.net/10464/3147
dc.description.abstractRelAPS is an interactive system assisting in proving relation-algebraic theorems. The aim of the system is to provide an environment where a user can perform a relation-algebraic proof similar to doing it using pencil and paper. The previous version of RelAPS accepts only Horn-formulas. To extend the system to first order logic, we have defined and implemented a new language based on theory of allegories as well as a new calculus. The language has two different kinds of terms; object terms and relational terms, where object terms are built from object constant symbols and object variables, and relational terms from typed relational constant symbols, typed relational variables, typed operation symbols and the regular operations available in any allegory. The calculus is a mixture of natural deduction and the sequent calculus. It is formulated in a sequent style but with exactly one formula on the right-hand side. We have shown soundness and completeness of this new logic which verifies that the underlying proof system of RelAPS is working correctly.en_US
dc.language.isoengen_US
dc.publisherBrock Universityen_US
dc.subjectRelation algebrasen_US
dc.subjectComputer science -- Mathematics.en_US
dc.titleExtending relAPS to first order logicen_US
dc.typeElectronic Thesis or Dissertationen_US
dc.degree.nameM.Sc. Computer Scienceen_US
dc.degree.levelMastersen_US
dc.contributor.departmentDepartment of Computer Scienceen_US
dc.degree.disciplineFaculty of Mathematics and Scienceen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record