Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
In recent years, G\"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first-order logic extended by predicate quantification. Formula macros are used to structure complex formulas and tasks. The analysis is presented as a generated type-set document where informal explanations are interspersed with pretty-printed formulas and outputs of reasoners for first-order theorem proving and second-order quantifier elimination. Previously unnoticed or obscured aspects and details of G\"odel's proof become apparent. Practical application possibilities of second-order quantifier elimination are shown and the encountered elimination tasks may serve as benchmarks.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingSimilar Papers 제목 키워드 기반
Second-Order Specifications and Quantifier Elimination for Consistent Query Answering in Databases
Consistent answers to a query from a possibly inconsistent database are answers that are simultaneously retrieved from every possible repair of the database. Repairs are consistent instances that minimally differ from th…
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
For relational monadic formulas (the L\"owenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, projection and forgetting - operations that currently receive …
PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents that intersperse macro definitions, reas…
Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
Cylindrical algebraic decomposition(CAD) is a key tool in computational algebraic geometry, particularly for quantifier elimination over real-closed fields. When using CAD, there is often a choice for the ordering placed…
BIG-bench Machine LearningFacets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. Its main focus is on formulas, as constituents of complex formalizations that are structured through formula macros, and as …