{"id":{"repo_id":"brock","oai_identifier":"oai:brocku.scholaris.ca:10464/4126"},"canonical_url":"https://search.dev.ndltd.org/etd/brock/oai:brocku.scholaris.ca:10464/4126","repository":{"repo_id":"brock","name":"Brock University","base_url":"https://brocku.scholaris.ca/server/oai/request"},"display":{"title":"A System for Models of First Order Theories","abstract":"If you want to know whether a property is true or not in a specific algebraic structure,you need to test that property on the given structure. This can be done by hand, which can be cumbersome and erroneous. In addition, the time consumed in testing depends on the size of the structure where the property is applied. We present an implementation of a system for finding counterexamples and testing properties of models of first-order theories. This system is supposed to provide a convenient and paperless environment for researchers and students investigating or studying such models and algebraic structures in particular. To implement a first-order theory in the system, a suitable first-order language.( and some axioms are required. The components of a language are given by a collection of variables, a set of predicate symbols, and a set of operation symbols. Variables and operation symbols are used to build terms. Terms, predicate symbols, and the usual logical connectives are used to build formulas. A first-order theory now consists of a language together with a set of closed formulas, i.e. formulas without free occurrences of variables. The set of formulas is also called the axioms of the theory. The system uses several different formats to allow the user to specify languages, to define axioms and theories and to create models. Besides the obvious operations and tests on these structures, we have introduced the notion of a functor between classes of models in order to generate more co~plex models from given ones automatically. As an example, we will use the system to create several lattices structures starting from a model of the theory of pre-orders.","abstract_html":"If you want to know whether a property is true or not in a specific algebraic structure,you need to test that property on the given structure. This can be done by hand, which can be cumbersome and erroneous. In addition, the time consumed in testing depends on the size of the structure where the property is applied. We present an implementation of a system for finding counterexamples and testing properties of models of first-order theories. This system is supposed to provide a convenient and paperless environment for researchers and students investigating or studying such models and algebraic structures in particular. To implement a first-order theory in the system, a suitable first-order language.( and some axioms are required. The components of a language are given by a collection of variables, a set of predicate symbols, and a set of operation symbols. Variables and operation symbols are used to build terms. Terms, predicate symbols, and the usual logical connectives are used to build formulas. A first-order theory now consists of a language together with a set of closed formulas, i.e. formulas without free occurrences of variables. The set of formulas is also called the axioms of the theory. The system uses several different formats to allow the user to specify languages, to define axioms and theories and to create models. Besides the obvious operations and tests on these structures, we have introduced the notion of a functor between classes of models in order to generate more co~plex models from given ones automatically. As an example, we will use the system to create several lattices structures starting from a model of the theory of pre-orders.","abstract_has_math":false,"creators":["AbdalBari, Anwar"],"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":2012,"date_issued":"2012-10-12","date_published":"2012-10-12","updated_at":"2026-07-24T01:23:05Z","subjects":["First order theories","Computer programming."],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10464/4126","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":["AbdalBari, Anwar"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2012-10-12T14:24:41Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2012-10-12T14:24:41Z"]},{"key":"dc:date.issued","label":"Date","values":["2012-10-12"]},{"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":["First order theories","Computer programming."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10464/4126"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["If you want to know whether a property is true or not in a specific algebraic structure,you need to test that property on the given structure. This can be done by hand, which can be cumbersome and erroneous. In addition, the time consumed in testing depends on the size of the structure where the property is applied. We present an implementation of a system for finding counterexamples and testing properties of models of first-order theories. This system is supposed to provide a convenient and paperless environment for researchers and students investigating or studying such models and algebraic structures in particular. To implement a first-order theory in the system, a suitable first-order language.( and some axioms are required. The components of a language are given by a collection of variables, a set of predicate symbols, and a set of operation symbols. Variables and operation symbols are used to build terms. Terms, predicate symbols, and the usual logical connectives are used to build formulas. A first-order theory now consists of a language together with a set of closed formulas, i.e. formulas without free occurrences of variables. The set of formulas is also called the axioms of the theory. The system uses several different formats to allow the user to specify languages, to define axioms and theories and to create models. Besides the obvious operations and tests on these structures, we have introduced the notion of a functor between classes of models in order to generate more co~plex models from given ones automatically. As an example, we will use the system to create several lattices structures starting from a model of the theory of pre-orders."]},{"key":"dc:title","label":"Title","values":["A System for Models of First Order Theories"]}]}],"canonical_facts":{"dc:contributor.department":["Department of Computer Science"],"dc:creator":["AbdalBari, Anwar"],"dc:date.accessioned":["2012-10-12T14:24:41Z"],"dc:date.available":["2012-10-12T14:24:41Z"],"dc:date.issued":["2012-10-12"],"dc:description.abstract":["If you want to know whether a property is true or not in a specific algebraic structure,you need to test that property on the given structure. This can be done by hand, which can be cumbersome and erroneous. In addition, the time consumed in testing depends on the size of the structure where the property is applied. We present an implementation of a system for finding counterexamples and testing properties of models of first-order theories. This system is supposed to provide a convenient and paperless environment for researchers and students investigating or studying such models and algebraic structures in particular. To implement a first-order theory in the system, a suitable first-order language.( and some axioms are required. The components of a language are given by a collection of variables, a set of predicate symbols, and a set of operation symbols. Variables and operation symbols are used to build terms. Terms, predicate symbols, and the usual logical connectives are used to build formulas. A first-order theory now consists of a language together with a set of closed formulas, i.e. formulas without free occurrences of variables. The set of formulas is also called the axioms of the theory. The system uses several different formats to allow the user to specify languages, to define axioms and theories and to create models. Besides the obvious operations and tests on these structures, we have introduced the notion of a functor between classes of models in order to generate more co~plex models from given ones automatically. As an example, we will use the system to create several lattices structures starting from a model of the theory of pre-orders."],"dc:identifier.uri":["http://hdl.handle.net/10464/4126"],"dc:subject":["First order theories","Computer programming."],"dc:title":["A System for Models of First Order Theories"],"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:23:05Z"}