{"id":{"repo_id":"brock","oai_identifier":"oai:brocku.scholaris.ca:10464/2928"},"canonical_url":"https://search.dev.ndltd.org/etd/brock/oai:brocku.scholaris.ca:10464/2928","repository":{"repo_id":"brock","name":"Brock University","base_url":"https://brocku.scholaris.ca/server/oai/request"},"display":{"title":"Towards automated derivation in the theory of allegories","abstract":"We provide an algorithm that automatically derives many provable theorems in the equational theory of allegories. This was accomplished by noticing properties of an existing decision algorithm that could be extended to provide a derivation in addition to a decision certificate. We also suggest improvements and corrections to previous research in order to motivate further work on a complete derivation mechanism. The results presented here are significant for those interested in relational theories, since we essentially have a subtheory where automatic proof-generation is possible. This is also relevant to program verification since relations are well-suited to describe the behaviour of computer programs. It is likely that extensions of the theory of allegories are also decidable and possibly suitable for further expansions of the algorithm presented here.","abstract_html":"We provide an algorithm that automatically derives many provable theorems in the equational theory of allegories. This was accomplished by noticing properties of an existing decision algorithm that could be extended to provide a derivation in addition to a decision certificate. We also suggest improvements and corrections to previous research in order to motivate further work on a complete derivation mechanism. The results presented here are significant for those interested in relational theories, since we essentially have a subtheory where automatic proof-generation is possible. This is also relevant to program verification since relations are well-suited to describe the behaviour of computer programs. It is likely that extensions of the theory of allegories are also decidable and possibly suitable for further expansions of the algorithm presented here.","abstract_has_math":false,"creators":["Glanfield, Joel."],"institution":"Brock University","degree_name":"M.Sc. Computer Science","degree_level":"Masters","degree_discipline":"Faculty of Mathematics and Science","degree_department":"Department of Computer Science","school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2008,"date_issued":"2008-02-16T15:46:03Z","date_published":"2008-02-16T15:46:03Z","updated_at":"2026-07-24T01:22:54Z","subjects":["Allegories (Mathematics)","Computer algorithms."],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10464/2928","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.department","label":"Department","values":["Department of Computer Science"]},{"key":"dc:creator","label":"Author","values":["Glanfield, Joel."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2010-02-16T15:46:03Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2010-02-16T15:46:03Z"]},{"key":"dc:date.issued","label":"Date","values":["2008-02-16T15:46:03Z"]},{"key":"dc:type","label":"Dc Type","values":["Electronic Thesis or Dissertation"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Faculty of Mathematics and Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.Sc. Computer Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Brock University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Allegories (Mathematics)","Computer algorithms."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10464/2928"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["We provide an algorithm that automatically derives many provable theorems in the equational theory of allegories. This was accomplished by noticing properties of an existing decision algorithm that could be extended to provide a derivation in addition to a decision certificate. We also suggest improvements and corrections to previous research in order to motivate further work on a complete derivation mechanism. The results presented here are significant for those interested in relational theories, since we essentially have a subtheory where automatic proof-generation is possible. This is also relevant to program verification since relations are well-suited to describe the behaviour of computer programs. It is likely that extensions of the theory of allegories are also decidable and possibly suitable for further expansions of the algorithm presented here."]},{"key":"dc:title","label":"Title","values":["Towards automated derivation in the theory of allegories"]}]}],"canonical_facts":{"dc:contributor.department":["Department of Computer Science"],"dc:creator":["Glanfield, Joel."],"dc:date.accessioned":["2010-02-16T15:46:03Z"],"dc:date.available":["2010-02-16T15:46:03Z"],"dc:date.issued":["2008-02-16T15:46:03Z"],"dc:description.abstract":["We provide an algorithm that automatically derives many provable theorems in the equational theory of allegories. This was accomplished by noticing properties of an existing decision algorithm that could be extended to provide a derivation in addition to a decision certificate. We also suggest improvements and corrections to previous research in order to motivate further work on a complete derivation mechanism. The results presented here are significant for those interested in relational theories, since we essentially have a subtheory where automatic proof-generation is possible. This is also relevant to program verification since relations are well-suited to describe the behaviour of computer programs. It is likely that extensions of the theory of allegories are also decidable and possibly suitable for further expansions of the algorithm presented here."],"dc:identifier.uri":["http://hdl.handle.net/10464/2928"],"dc:language.iso":["eng"],"dc:subject":["Allegories (Mathematics)","Computer algorithms."],"dc:title":["Towards automated derivation in the theory of allegories"],"dc:type":["Electronic Thesis or Dissertation"],"thesis:degree_discipline":["Faculty of Mathematics and Science"],"thesis:degree_level":["Masters"],"thesis:degree_name":["M.Sc. Computer Science"],"thesis:institution_name":["Brock University"]},"updated_at":"2026-07-24T01:22:54Z"}