Digital Repository

Extending relAPS to first order logic

DSpace/Manakin Repository

Show simple item record

dc.contributor.author Aameri, Bahar
dc.date.accessioned 2011-03-08T16:55:24Z
dc.date.available 2011-03-08T16:55:24Z
dc.date.issued 2011-03-08
dc.identifier.uri http://hdl.handle.net/10464/3147
dc.description.abstract RelAPS 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.iso eng en_US
dc.publisher Brock University en_US
dc.subject Relation algebras en_US
dc.subject Computer science -- Mathematics. en_US
dc.title Extending relAPS to first order logic en_US
dc.type Electronic Thesis or Dissertation en_US
dc.degree.name M.Sc. Computer Science en_US
dc.degree.level Masters en_US
dc.contributor.department Department of Computer Science en_US
dc.degree.discipline Faculty of Mathematics and Science en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search The Repository


Browse

My Account

Statistics


About the Digital Repository