Contemporary related work
Contemporary work in applied formal reasoning for science and engineering: institution theory in physics and systems engineering, higher-order logic for the natural sciences, formal ontologies for engineering and chemistry, Homotopy Type Theory and its directed and dynamic extensions, and the epistemology of formal proof.
Generated from docs/references/eigenius_related_work.bib by scripts/bib-to-md.py. Do not edit by hand.
Total entries: 30.
awodey-warren2009
Awodey, Steve and Warren, Michael A. (2009). “Homotopy theoretic models of identity types”. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1), pp. 45–55.
DOI: 10.1017/S0305004108001783
Establishes the homotopy-theoretic interpretation of Martin-Löf identity types — a precursor to the univalent foundations program.
birkhoff-vonneumann1936
Birkhoff, Garrett and von Neumann, John (1936). “The logic of quantum mechanics”. Annals of Mathematics, 37(4), pp. 823–843.
Founding paper of quantum logic; introduces the orthomodular lattice structure of quantum events as an alternative to classical Boolean algebra.
borgo-mizoguchi2009
Borgo, Stefano and Mizoguchi, Riichiro (2009). “A formal ontological perspective on the behaviors and functions of technical artifacts”. AI EDAM (Artificial Intelligence for Engineering Design, Analysis and Manufacturing), 23(1), pp. 3–21.
DOI: 10.1017/S0890060409000079
Uses DOLCE to give a uniform formal account of artifact behavior vs. function — a long-standing source of miscommunication in engineering design.
darrigol2008-modular
Darrigol, Olivier (2008). “The modular structure of physical theories”. Synthese, 162(2), pp. 195–223.
DOI: 10.1007/s11229-007-9181-x
Argues that mature physical theories decompose into modules with stable interfaces — the philosophical analogue of the colimit-style composition that institutions formalize.
fca-process-ontologies
Tutcher, Jonathan (2014). “A Formal Concept Analysis-based method for developing process ontologies, applied to chemical engineering”. In Proceedings of an industrial-ontology workshop.
Uses FCA to derive class hierarchies for chemical engineering processes and integrates them with ISO 15926 / SUMO. Exact venue per ResearchGate publication 271505148.
garbacz-engineering-functions
Garbacz, Paweł, et al.. “Towards a formal ontology of engineering functions, behaviours, and capabilities”. Semantic Web Journal.
Submission swj3188; surveys formalizations of engineering function/behaviour/capability and proposes a unifying ontology.
genetic-code-hott
Anonymous (2024). “Exploring the genetic code: A Homotopy Type Theory approach to uncovering embedded information”. Preprint.
Analyzes codon relationships and nucleotide permutations in a 3D lattice model under HoTT; surfaces structure suggestive of layered molecular language. ResearchGate publication 380075492; authorship to be verified.
glymour2013-theoretical-equivalence
Glymour, Clark (2013). “Theoretical equivalence and the semantic view of theories”. Philosophy of Science, 80(2), pp. 286–297.
Response to Halvorson 2012. The user’s reading list links this title to an institution-theoretic treatment with quantum cosmology examples; the title matches Glymour’s paper exactly, but Glymour’s paper itself does not use institutions — it defends the semantic view via De Bouvere’s criteria. The institution-theoretic angle on this debate is in Halvorson & Tsementzis, “Categories of Scientific Theories” (2017).
halvorson2012
Halvorson, Hans (2012). “What scientific theories could not be”. Philosophy of Science, 79(2), pp. 183–206.
Critique of the strict semantic view of scientific theories; starts the debate that motivates institution- and category-theoretic accounts.
herre2010gfo
Herre, Heinrich (2010). “General Formal Ontology (GFO): A foundational ontology for conceptual modelling”. In Theory and Applications of Ontology: Computer Applications, ed. Poli, Roberto, Healy, Michael, and Kameas, Achilles, pp. 297–345, Springer.
Specification of GFO, an integrative axiomatic top-level ontology used as a peer to BFO and DOLCE.
kent-iff2011
Kent, Robert E. (2011). The Information Flow Framework: A descriptive category metatheory.
Structural metatheory for the IEEE P1600.1 Standard Upper Ontology (SUO) project; uses institutions and their morphisms as the upper-metalevel axiomatization for semantic integration of ontologies.
khan-afshar-complex-vectors
Khan-Afshar, Sanaz, Siddique, Umair, Mahmoud, Muhammad Yasir, Hasan, Osman, and Tahar, Sofiène (2014). “Formalization of complex vectors in higher-order logic”. In CICM 2014: International Conference on Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence 8543, pp. 123–137, Springer.
HOL Light formalization of complex vector analysis used to verify foundational laws of electromagnetism.
knapp-institutional-framework-uml2015
Knapp, Alexander, Mossakowski, Till, and Roggenbach, Markus (2015). “Towards an institutional framework for heterogeneous formal development in UML — A position paper”. In Software, Services, and Systems: Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, ed. De Nicola, Rocco and Hennicker, Rolf, Lecture Notes in Computer Science 8950, pp. 215–230, Springer.
DOI: 10.1007/978-3-319-15545-6_15
knapp-uml-state-machines2015
Knapp, Alexander, Mossakowski, Till, Roggenbach, Markus, and Glauer, Martin (2015). “An institution for simple UML state machines”. In FASE 2015: Fundamental Approaches to Software Engineering, ed. Egyed, Alexander and Schaefer, Ina, Lecture Notes in Computer Science 9033, pp. 3–18, Springer.
DOI: 10.1007/978-3-662-46675-9_1
martinot2024ontological-purity
Martinot, Robin (2024). “Ontological purity for formal proofs”. The Review of Symbolic Logic, 17(2), pp. 395–434.
DOI: 10.1017/S1755020323000333
Develops a graded notion of ontological purity for formal proofs, including a notion of “secondary purity” for proofs that use surrogate content via formal interpretations. Directly relevant to evaluating cross-layer reasoning in Eigenius.
masolo2003dolce
Masolo, Claudio, Borgo, Stefano, Gangemi, Aldo, Guarino, Nicola, and Oltramari, Alessandro (2003). “WonderWeb Deliverable D18: Ontology Library”. Laboratory For Applied Ontology (ISTC-CNR).
Foundational specification of DOLCE (Descriptive Ontology for Linguistic and Cognitive Engineering).
model-management-syseng-kg
Anonymous (2025). Model management to support systems engineering workflows using ontology-based knowledge graphs.
Uses the Ontology Modelling Language (OML) to relate systems engineering processes to artifacts via a knowledge graph; supports versioning and reasoning.
ontology-based-plm-polimi
Polimi authors (2025). “Ontology-based product lifecycle management: Insights from a proof-of-concept implementation”. IEEE Access.
Demonstrates ontology-driven PLM in an Engineer-to-Order setting; combines linked-data infrastructure with description-logic reasoning. Authorship per Polimi repository entry; exact attribution should be verified.
ontology-of-physics-for-biology
Cook, Daniel L., Bookstein, Fred L., and Gennari, John H. (2011). “Physical properties of biological entities: An introduction to the Ontology of Physics for Biology”. PLOS ONE, 6(12), pp. e28708.
DOI: 10.1371/journal.pone.0028708
Specification of OPB, which extends BFO with energy-bearing biophysical entities and quantitative dependencies.
poernomo2025dhott
Poernomo, Iman (2025). DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift.
Indexes types by a context-time parameter so they may deform, rupture, and reassemble — supports formal reasoning about semantic evolution and discontinuity.
psrl-nist
Patil, Lalit, Dutta, Debasish, and Sriram, Ram D. (2005). “Ontology Formalization of Product Semantics for Product Lifecycle Management”. National Institute of Standards and Technology, NISTIR 7274.
Defines the Product Semantic Representation Language (PSRL), a description-logic-based formalism for application-independent product semantics in PLM.
qiu2025state-formalization
Qiu, others (2025). “Research on a general state formalization method from the perspective of logic”. Mathematics (MDPI), 13(20), pp. 3324.
Proposes a unified axiomatization of states as interpretations of formulas across first-order, higher-order, and infinitary logics. Full author list per Crossref starts with Qiu; complete attribution should be filled in from the MDPI page before any citation use.
rashid-hasan-systems-biology
Rashid, Adnan, Hasan, Osman, Siddique, Umair, and Tahar, Sofiène (2017). “Formal reasoning about systems biology using theorem proving”. PLOS ONE, 12(7), pp. e0180179.
DOI: 10.1371/journal.pone.0180179
Formalizes Zsyntax in HOL4 / HOL Light for the verification of molecular pathways and biological networks.
rashid-laplace-fourier
Rashid, Adnan and Hasan, Osman. “Formalization of Laplace and Fourier transforms in higher-order logic for the analysis of synthetic biology genetic circuits”. Theoretical Computer Science (or related).
Frequency-domain analysis of synthetic genetic circuits carried out in HOL Light; exact venue should be confirmed. Source: cited by the survey at PMC5495343.
siddique2015thesis
Siddique, Umair (2015). Formal Analysis of Fractional Order Systems in Higher-Order Logic. PhD thesis, Concordia University.
Develops a HOL Light library for fractional-order systems and applies it to engineering analysis.
smith2012classifying-processes
Smith, Barry (2012). “Classifying processes: An essay in applied ontology”. Ratio (new series), 25(4), pp. 463–488.
DOI: 10.1111/j.1467-9329.2012.00557.x
Articulates the BFO treatment of occurrents (processes) and their classification.
sowa-signs-processes
Sowa, John F. (2010). Signs, Processes, and Language Games: Foundations for Ontology. Online manuscript, jfsowa.com.
Sowa’s foundational essay arguing that ontology must account for signs, processes, and language games — a framing closely related to Eigenius’s typed-layer view of scientific knowledge.
voevodsky2014univalent
Voevodsky, Vladimir (2014). The Origins and Motivations of Univalent Foundations. The Institute Letter, Institute for Advanced Study.
Voevodsky’s own account of the genesis of univalent foundations and the univalence axiom.
weaver-bicubical-dtt
Weaver, Matthew Z. (2024). Bicubical Directed Type Theory. PhD thesis, Princeton University.
Generalizes groupoid-style HoTT to a directed setting with morphisms — a foundation for type-theoretic reasoning over directed processes.
zhou2023marie-bert
Zhou, Xiaochi, Zhang, Shaocong, Agarwal, Mehal, Akroyd, Jethro, Mosbach, Sebastian, and Kraft, Markus (2023). “Marie and BERT—A knowledge graph embedding based question answering system for chemistry”. ACS Omega, 8(36), pp. 33039–33057.
Combines hybrid knowledge graph embeddings with BERT-based entity linking to answer multihop chemistry questions over OntoSpecies / OntoMOPs.