Online research in philosophy

The automatic verification of large parts of mathematics has been an aim of many mathematicians from Leibniz to Hilbert. While Gödel's first incompleteness theorem showed that no computer program could automatically prove certain true theorems in mathematics, the advent of electronic computers and sophisticated software means in practice there are many quite effective systems for automated reasoning that can be used for checking mathematical proofs. This book describes the use of a computer program to check the proofs of several celebrated theorems in metamathematics including those of Gödel and Church-Rosser. The computer verification using the Boyer-Moore theorem prover yields precise and rigorous proofs of these difficult theorems. It also demonstrates the range and power of automated proof checking technology. The mechanization of metamathematics itself has important implications for automated reasoning, because metatheorems can be applied as labor-saving devices to simplify proof construction.

Certain distributivity results for Lukasiewicz’s infinite-valued logic Lℵ0 are proved axiomatically (for the first time) with the help of the automated reasoning program Otter [16]. In addition, non -distributivity results are established for a wide variety of positive substructural logics by the use of logical matrices discovered with the automated model findingprograms Mace [15] and MaGIC [25].

Notions of disambiguation supporting a compositional interpretation ofvambiguous expressions and reflecting intuitions about how sentences combinevin discourse are investigated. Expressions are analyzed both inductively byvbreaking them apart, and co-inductively by embedding them within larger contexts.

he goal of this article is to formalize Object Role Modeling (ORM) using the DLR description logic. This would enable automated reasoning on the formal properties of ORM diagrams, such as detecting constraint contradictions and implications. In addition, the expressive, methodological, and graphical capabilities of ORM make it a good candidate for use as a graphical notation for most description logic languages. In this way, industrial experts who are not IT savvy will still be able to build and view axiomatized theories (such as ontologies, business rules, etc.) without needing to know the logic or reasoning foundations underpinning them. Our formalization in this paper is structured as 29 formalization rules, that map all ORM primitives and constraints into DLR, and 2 exceptions of complex cases. To this end, we illustrate the implementation of our formalization as an extension to DogmaModeler, which automatically maps ORM into DIG and uses Racer as a background reasoning engine to reason about ORM diagrams.

In this paper, the authors describe their initial investigations in computational metaphysics. Our method is to implement axiomatic metaphysics in an automated reasoning system. In this paper, we describe what we have discovered when the theory of abstract objects is implemented in prover9 (a first-order automated reasoning system which is the successor to otter). After reviewing the second-order, axiomatic theory of abstract objects, we show (1) how to represent a fragment of that theory in prover9’s first-order syntax, and (2) how prover9 then finds proofs of interesting theorems of metaphysics, such as that every possible world is maximal. We conclude the paper by discussing some issues for further research.

In this article a dialectical model for practical reasoning within a community, based on the Generic/Actual Argument Model (GAAM) is advanced and its application to deliberative dialogue discussed. The GAAM, offers a dynamic template for structuring knowledge within a domain of discourse that is connected to and regulated by a community. The paper demonstrates how the community accepted generic argument structure acts to normatively influence both admissible reasoning and the progression of dialectical reasoning between participants. It is further demonstrated that these types of deliberation dialogues supported by the GAAM comply with criteria for normative principles for deliberation, specifically, Alexy’s rules for discourse ethics and Hitchcock’s Principles of Rational Mutual Inquiry. The connection of reasoning to the community in a documented and transparent structure assists in providing best justified reasons, principles of deliberation and ethical discourse which are important advantages for reasoning communities.

The resolution of ambiguities is one of the central problems for Machine Translation. In this paper we propose a knowledge-based approach to disambiguation which uses Description Logics (dl) as representation formalism. We present the process of anaphora resolution implemented in the Machine Translation systemfast and show how thedl systemback is used to support disambiguation.The disambiguation strategy uses factors representing syntactic, semantic, and conceptual constraints with different weights to choose the most adequate antecedent candidate. We show how these factors can be declaratively represented as defaults inback. Disambiguation is then achieved by determining the interpretation that yields a qualitatively minimal number of exceptions to the defaults, and can thus be formalized as exception minimization.

We present a preliminary study on disambiguation of symbolic expressions in mathematical documents. We propose to use the natural language within which the expressions are embedded to resolve their semantics. The approach is based on establishing a similarity between the expression’s discourse context and a set of terms from Term Clusters based on OpenMath Content Dictionaries. The Term Clusters are semi-automatically constructed terminological resources which classify related mathematical concepts into groups. Each group is labelled with a term which represents the common denominator between the concepts.

There are few successful applications of automated reasoning over OWL-formalised bio-ontologies, and requirements are often unclearly formulated. Of what is available, usage and prospective scenarios of automated reasoning is often different from the straightforward classification and satisfiability. We list nine types of scenarios and specify the requirements in more detail. Several of these requirements are already possible in practice or at least in theory, others are in need of further research, in particular regarding the linking of the OWL ontology to data, reasoning over roles, and dynamically linking modular ontologies.