MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY

DOI10.1017/S1755020319000297zbMath1484.03020arXiv1711.06542OpenAlexW3102415061MaRDI QIDQ5221294

Christoph Benzmüller, Daniel Kirchner, Edward N. Zalta

Publication date: 25 March 2020

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1711.06542

zbMATH Keywords

theorem provinghigher-order logicshallow semantical embeddinguniversal reasoningcomputational metaphysicsabstract object theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Philosophical and critical aspects of logic and foundations (03A05) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Related Items (4)

Is weak supplementation analytic? ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts ⋮ PLM

Uses Software

• Isabelle/HOL
• Archive Formal Proofs

Cites Work

• Worlds and propositions set free
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• Isabelle/HOL. A proof assistant for higher-order logic
• Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
• Intensional models for the theory of types
• Not Every Object of Thought has Being: A Paradox in Naive Predication Theory

This page was built for publication: MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY