GoedelGod
From MaRDI portal
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- A deontic logic reasoning infrastructure
- A dyadic deontic logic in HOL
- A first-order conditional logic for prototypical properties
- A formulation of the simple theory of types.
- A new small emendation of Gödel's ontological proof
- Agent-based HOL reasoning
- All properties are divine or god exists -- the sacred thesis and its ontological argument
- An introduction to mathematical logic and type theory: To truth through proof.
- An object-logic explanation for the inconsistency in Gödel's ontological theory
- Automating emendations of the ontological argument in intensional higher-order modal logic
- Automating free logic in HOL, with an experimental application in category theory
- Automating free logic in Isabelle/HOL
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Automating Leibniz's theory of concepts
- Basic conditional logic
- Categorical logic and type theory
- Coalgebraic logic
- Combining and automating classical and non-classical logics in classical higher-order logics
- Comparing approaches to resolution based higher-order theorem proving
- Completeness and decidability results for a logic of contrary-to-duty conditionals
- Computer supported mathematics with MEGA
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel's ontological argument
- Computer-supported exploration of a categorical axiomatization of modeloids
- Conceptual notation.
- Cut-elimination for quantified conditional logic
- Cut-Simulation and Impredicativity
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Encoding two-valued nonclassical logics in classical logic
- Extending Sledgehammer with SMT solvers
- First-order conditional logic for default reasoning revisited
- Generic modal cut elimination applied to conditional logics
- Groups, Categories and Duality
- Higher-order modal logics: automation and applications
- Higher-order semantics and extensionality
- HOL Based First-Order Modal Logic Provers
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Implementing and evaluating provers for first-order modal logics
- Input/output logics
- Interacting with Modal Logics in the Coq Proof Assistant
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Mechanizing \textit{Principia logico-metaphysica} in functional type-theory
- Modal Logic as Metaphysics
- More SPASS with Isabelle
- Multimodal and intuitionistic logics in simple type theory
- Natural numbers and natural cardinals as abstract objects: A partial reconstruction of Frege's \textit{Grundgesetze} in object theory
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- On connections and higher-order logic
- On first-order conditional logics
- On logic embeddings and Gödel's God
- On the fine-structure of regular algebra
- Principia Mathematica. Vol. I.
- Quantified multimodal logics in simple type theory
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
- Resource-Adaptive Cognitive Processes
- Satallax: An Automatic Higher-Order Prover
- Steps toward a computational metaphysics
- Sufficient conditions for cut elimination with complexity analysis
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- System description: E 1.8
- The higher-order prover Leo-III
- Theorem provers for every normal modal logic
- Twenty-five basic theorems in situation and world theory
- Types, tableaus, and Gödel's God
- Universal coalgebra: A theory of systems
- Variants of Gödel's ontological proof in a natural deduction calculus
Cited in
(10)- RuleML
- Variants of Gödel's ontological proof in a natural deduction calculus
- AgsyHOL
- Gen2sat
- Interacting with Modal Logics in the Coq Proof Assistant
- Para-disagreement logics and their implementation through embedding in Coq and SMT
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- intuit
- Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel's ontological argument
- scientific article; zbMATH DE number 7178360 (Why is no real title available?)
This page was built for software: GoedelGod
