{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:57153"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:57153","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Guarded logics : algorithms and bisimulation","abstract":"For many practical applications of logic-based methods there is a requirement to balance expressive power against computational tractability. Both identifying decidable sub-classes of first-order logic, and extending modal logic to larger, but nevertheless efficiently solvable languages has been a preeminent goal of research. The guarded fragment of first-order logic was a successful attempt to transfer key tractability properties of modal, temporal, and description logics to a larger fragment of predicate logic. Besides decidability, guarded logics inherit the finite model property, invariance under an appropriate variant of bisimulation, and other nice model theoretic properties including a decidable fixed-point extension. The goal of this this work is to gain greater insight into the correspondence between the modal world and the guarded world. In this process, several gaps concerning basic, typically modal, features of guarded logics are closed. Guarded second order logic and guarded relational algebra are developed. A recurring key technique consists of encoding structures and formulae used in the guarded world as their modal counterparts. This enables the transfer of various results, as well as giving greater insight into the nature of guarded logics. Touched subjects include tableau-based decision procedures, mapping action guarded logics, canonisation of structures and model-theoretic characterisation theorems.","abstract_html":"For many practical applications of logic-based methods there is a requirement to balance expressive power against computational tractability. Both identifying decidable sub-classes of first-order logic, and extending modal logic to larger, but nevertheless efficiently solvable languages has been a preeminent goal of research. The guarded fragment of first-order logic was a successful attempt to transfer key tractability properties of modal, temporal, and description logics to a larger fragment of predicate logic. Besides decidability, guarded logics inherit the finite model property, invariance under an appropriate variant of bisimulation, and other nice model theoretic properties including a decidable fixed-point extension. The goal of this this work is to gain greater insight into the correspondence between the modal world and the guarded world. In this process, several gaps concerning basic, typically modal, features of guarded logics are closed. Guarded second order logic and guarded relational algebra are developed. A recurring key technique consists of encoding structures and formulae used in the guarded world as their modal counterparts. This enables the transfer of various results, as well as giving greater insight into the nature of guarded logics. Touched subjects include tableau-based decision procedures, mapping action guarded logics, canonisation of structures and model-theoretic characterisation theorems.","abstract_has_math":false,"creators":["Hirsch, Colin"],"institution":"Publikationsserver der RWTH Aachen University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Grädel, Erich"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2002,"date_issued":"2002","date_published":"2002","updated_at":"2026-07-30T19:42:09Z","subjects":["info:eu-repo/classification/ddc/004","Informatik","mathematische Logik","Modelltheorie","Bisimulation"],"languages":["eng"],"rights":["info:eu-repo/semantics/openAccess"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-119220%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-119220%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-119220%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/57153","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Grädel, Erich"]},{"key":"dc:creator","label":"Author","values":["Hirsch, Colin"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:coverage","label":"Dc Coverage","values":["DE"]},{"key":"dc:date","label":"Dc Date","values":["2002"]},{"key":"dc:publisher","label":"Institution","values":["Publikationsserver der RWTH Aachen University"]},{"key":"dc:relation","label":"Dc Relation","values":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-4550"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["info:eu-repo/classification/ddc/004","Informatik","mathematische Logik","Modelltheorie","Bisimulation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/openAccess"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/record/57153","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-119220%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["For many practical applications of logic-based methods there is a requirement to balance expressive power against computational tractability. Both identifying decidable sub-classes of first-order logic, and extending modal logic to larger, but nevertheless efficiently solvable languages has been a preeminent goal of research. The guarded fragment of first-order logic was a successful attempt to transfer key tractability properties of modal, temporal, and description logics to a larger fragment of predicate logic. Besides decidability, guarded logics inherit the finite model property, invariance under an appropriate variant of bisimulation, and other nice model theoretic properties including a decidable fixed-point extension. The goal of this this work is to gain greater insight into the correspondence between the modal world and the guarded world. In this process, several gaps concerning basic, typically modal, features of guarded logics are closed. Guarded second order logic and guarded relational algebra are developed. A recurring key technique consists of encoding structures and formulae used in the guarded world as their modal counterparts. This enables the transfer of various results, as well as giving greater insight into the nature of guarded logics. Touched subjects include tableau-based decision procedures, mapping action guarded logics, canonisation of structures and model-theoretic characterisation theorems."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : Publikationsserver der RWTH Aachen University 156 S. : graph. Darst. (2002). = Aachen, Techn. Hochsch., Diss., 2002"]},{"key":"dc:title","label":"Title","values":["Guarded logics : algorithms and bisimulation"]}]}],"canonical_facts":{"dc:contributor":["Grädel, Erich"],"dc:coverage":["DE"],"dc:creator":["Hirsch, Colin"],"dc:date":["2002"],"dc:description":["For many practical applications of logic-based methods there is a requirement to balance expressive power against computational tractability. Both identifying decidable sub-classes of first-order logic, and extending modal logic to larger, but nevertheless efficiently solvable languages has been a preeminent goal of research. The guarded fragment of first-order logic was a successful attempt to transfer key tractability properties of modal, temporal, and description logics to a larger fragment of predicate logic. Besides decidability, guarded logics inherit the finite model property, invariance under an appropriate variant of bisimulation, and other nice model theoretic properties including a decidable fixed-point extension. The goal of this this work is to gain greater insight into the correspondence between the modal world and the guarded world. In this process, several gaps concerning basic, typically modal, features of guarded logics are closed. Guarded second order logic and guarded relational algebra are developed. A recurring key technique consists of encoding structures and formulae used in the guarded world as their modal counterparts. This enables the transfer of various results, as well as giving greater insight into the nature of guarded logics. Touched subjects include tableau-based decision procedures, mapping action guarded logics, canonisation of structures and model-theoretic characterisation theorems."],"dc:identifier":["https://publications.rwth-aachen.de/record/57153","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-119220%22"],"dc:language":["eng"],"dc:publisher":["Publikationsserver der RWTH Aachen University"],"dc:relation":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-4550"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : Publikationsserver der RWTH Aachen University 156 S. : graph. Darst. (2002). = Aachen, Techn. Hochsch., Diss., 2002"],"dc:subject":["info:eu-repo/classification/ddc/004","Informatik","mathematische Logik","Modelltheorie","Bisimulation"],"dc:title":["Guarded logics : algorithms and bisimulation"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:42:09Z"}