Cited By
View all- Grüninger MChow AWong J(2023)Semiautomatic Design of OntologiesThe Practice of Enterprise Modeling10.1007/978-3-031-48583-1_9(143-158)Online publication date: 25-Nov-2023
Reducible Theories and Amalgamations of Models
Article No.: 9, Pages 1 - 24
Abstract
Within knowledge representation in artificial intelligence, a first-order ontology is a theory in first-order logic that axiomatizes the concepts in some domain. Ontology verification is concerned with the relationship between the intended models of an ontology and the models of the axiomatization of the ontology. In particular, we want to characterize the models of an ontology up to isomorphism and determine whether or not these models are equivalent to the intended models of the ontology. Unfortunately, it can be quite difficult to characterize the models of an ontology up to isomorphism. In the first half of this article, we review the different metalogical relationships between first-order theories and identify which relationship is needed for ontology verification. In particular, we will demonstrate that the notion of logical synonymy is needed to specify a representation theorem for the class of models of one first-order ontology with respect to another. In the second half of the article, we discuss the notion of reducible theories and show we can specify representation theorems by which models are constructed by amalgamating models of the constituent ontologies.
References
[1]
M. Grüninger and B. Aamerir. 2014. Preservation of modules. In Proceedings of the 8th International Workshop on Modular Ontologies. CEUR-WS.org.
[2]
B. Aameri and M. Gruninger. 2015. A new look at ontology correctness. In Proceedings of the AAAI Spring Symposium Series. AAAI Press, Palo Alto, 2–8.
[3]
N. Asher and L. Vieu. 1995. Toward a geometry of common sense: A semantics and a complete axiomatization of mereotopology. In International Joint Conference on Artificial Intelligence. Morgan Kaufmann Publishers Inc., 846–852.
[4]
M. Bidoit, D. Sannela, and A. Tarlecki. 2002. Architectural specifications in CASL. Form. Asp. Comput. 13 (2002), 252–273.
[5]
T. Bittner and M. Donnelly. 2007. Logical properties of foundational relations in bio-ontologies. Artif. Intell. Med. 39, 3 (2007), 197–216.
[6]
C. Bock and M. Gruninger. 2005. PSL: A semantic domain for flow models. Softw. Syst. Model. 4, 2 (2005), 209–231.
[7]
George Boolos, John P. Burgess, and Richard C. Jeffrey. 2002. Computability and Logic. Cambridge University Press, Cambridge, MA.
[8]
R. Casati and A. C. Varzi. 1999. Parts and Places: The Structures of Spatial Representation. MIT Press, Cambridge, MA.
[9]
A. G. Cohn, B. Bennett, J. Gooday, and N. Gotts. 1997. RCC: A calculus for region-based qualitative spatial reasoning. GeoInformatica 1 (1997), 275–316.
[10]
H. Enderton. 1972. Mathematical Introduction to Logic. Academic Press, Cambridge, MA.
[11]
W. M. Farmer. 2000. An infrastructure for intertheory reasoning. In Proceedings of the 17th International Conference on Automated Deduction (CADE), LNCS 1831. Springer, 115–131.
[12]
W. M. Farmer, J. D. Guttman, and F. J. Thayer. 1992. An infrastructure for intertheory reasoning. In Proceedings of the 11th International Conference on Automated Deduction (CADE), LNCS 607. Springer, 567–581.
[13]
M. Gruninger. 2003. Ontology of the process specification language. In Handbook on Ontologies in Information Systems. Springer-Verlag, Berlin, Germany.
[14]
Michael Gruninger. 2009. Definability and process ontologies. In Proceedings of the 9th International Symposium on Logical Formalizations of Commonsense Reasoning. AAAI, 53–58.
[15]
M. Gruninger. 2009. The ontological stance. J. Cases Inf. Syst. 4 (2009), 1–25.
[16]
Michael Grüninger. 2011. Verification of the OWL-time ontology. In Proceedings of the 10th International Semantic Web Conference (ISWC). Springer, 225–240.
[17]
Michael Gruninger, Carmen Chui, and Megan Katsumi. 2017. Upper ontologies in COLORE. In Proceedings of the Joint Ontology Workshops 2017 Episode 3: The Tyrolean Autumn of Ontology(CEUR Workshop Proceedings, Vol. 2050) Retrieved from http://ceur-ws.org/Vol-2050.
[18]
M. Gruninger, T. Hahmann, A. Hashemi, and D. Ong. 2010. Ontology verification with repositories. In Proceedings of the 6th International Conference on Formal Ontology in Information Systems. IOS Press, 317–330.
[19]
M. Grüninger, T. Hahmann, A. Hashemi, D. Ong, and A. Ozgovde. 2012. Modular first-order ontologies via repositories. Appl. Ontol. 7, 2 (2012), 169–209.
[20]
Michael Gruninger and Darren Ong. 2011. Verification of time ontologies with points and intervals. In Proceedings of the 18th International Symposium on Temporal Representation and Reasoning. IEEE, Piscataway, 31–38.
[21]
Nicola Guarino, Daniel Oberle, and Steffen Staab. 2009. What is an ontology? In Handbook on Ontologies. Springer, Berlin, Germany, 1–17.
[22]
D. Hilbert. 1899. Foundations of Geometry. Open Court, Chicago, IL.
[23]
Wilfrid Hodges. 1993. Model Theory. Cambridge University Press, Cambridge, MA.
[24]
Oliver Kutz and Till Mossakowski. 2011. A modular consistency proof for DOLCE. In Proceedings of the 25th AAAI Conference on Artificial Intelligence. AAAI, 227–234. Retrieved from http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3754.
[25]
David Marker. 2002. Model Theory: An Introduction. Springer, Berlin, Germany.
[26]
Lydia Silva Muñoz and Michael Grüninger. 2016. Mapping and verification of the time ontology in SUMO. In Proceedings of the 9th International Conference on Formal Ontology in Information Systems. IOS Press, 109–122. DOI:
[27]
R. Padmanabhan and S. Rudeanu. 2008. Axioms for Lattices and Boolean Algebras. World Scientific, Singapore.
[28]
D. Pearce and A. Valverde. 2012. Synonymous theories and knowledge representations in answer set programming. J. Comput. Syst. Sci. 78 (2012), 86–104.
[29]
A. Pillay and A. Tsuboi. 1997. Amalgamations preserving \(\aleph _1\)-categoricity. J. Symbol. Logic 62, 4 (1997), 1070–1074.
[30]
R. Reiter. 2001. Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. MIT Press, Cambridge, MA.
[31]
Barry Smith Robert Arp and Andrew Spear. 2015. Building Ontologies with Basic Formal Ontology. MIT Press, Cambridge, MA.
[32]
Joseph R. Shoenfield. 1967. Mathematical Logic. Addison-Wesley Reading, Boston, MA.
[33]
J. G. Stell. 2000. Boolean connection algebras: A new approach to the region-connection calculus. Artif. Intell. 122, 1–2 (2000), 111–136.
[34]
L. W. Szczerba. 1977. Interpretability of elementary theories. In Logic, Foundations of Mathematics and Computability Theory. Springer, Berlin, Germany, 129–145.
[35]
Andrzej Tarlecki. 1986. Bits and pieces of the theory of institutions. In Category Theory and Computer Programming. Springer, Berlin, Germany, 334–363.
[36]
Alfred Tarski. 1951. What is elementary geometry? In Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, Amsterdam, Netherlands, 16–29.
[37]
Albert Visser. 2006. Categories of theories and interpretations. In Logic in Tehran (Lecture Notes in Logic, Vol. 26). Association for Symbolic Logic, Tehran, Iran, 284–341.
[38]
R. Young. 2015. Reference ontologies for interoperability across multiple assembly systems. Int. J. Product. Res. 54 (2015), 5381–5403.
Index Terms
- Reducible Theories and Amalgamations of Models
Recommendations
Representing model theory in a type-theoretical logical framework
In a broad sense, logic is the field of formal languages for knowledge and truth that have a formal semantics. It tends to be difficult to give a narrower definition because very different kinds of logics exist. One of the most fundamental contrasts is ...
Modelling Generic Judgements
We propose a semantics for the @?-quantifier of Miller and Tiu. First we consider the case for classical first-order logic. In this case, the interpretation is close to standard Tarski-semantics and completeness can be shown using a standard argument. ...
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
AbstractWe discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with ...
Comments
Information & Contributors
Information
Published In
January 2023
326 pages
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 January 2023
Online AM: 29 September 2022
Accepted: 28 August 2022
Revised: 27 May 2022
Received: 19 August 2021
Published in TOCL Volume 24, Issue 1
Check for updates
Author Tags
Qualifiers
- Research-article
- Refereed
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 142Total Downloads
- Downloads (Last 12 months)30
- Downloads (Last 6 weeks)2
Reflects downloads up to 29 Jan 2025
Other Metrics
Citations
Cited By
View all- Grüninger MChow AWong J(2023)Semiautomatic Design of OntologiesThe Practice of Enterprise Modeling10.1007/978-3-031-48583-1_9(143-158)Online publication date: 25-Nov-2023
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderFull Text
View this article in Full Text.
Full TextHTML Format
View this article in HTML Format.
HTML Format