We introduce the logic of positive and negative contingency. Together with modal operators of necessity and impossibility they allow to dispense of negation. We study classes of Kripke models where the number of points is restricted, and show that the modalities reduce in the corresponding logics.

Preference-based reasoning is a form of commonsense reasoning that makes many problems easier to express and sometimes more likely to have a solution. We present an approach to introduce preferences in the weight constraint construct, which is a very useful programming construct widely adopted in Answer Set Programming (ASP). We show the usefulness of the proposed extension, and we outline how to accordingly extend the ASP semantics.

The Jobs Puzzle, introduced in a book about automated reasoning, is a logic puzzle solvable by some "intelligent sixth graders," but the formalization of the puzzle by the authors was, according to them, "sometimes difficult and sometimes tedious." The puzzle thus presents a triple challenge: 1) formalize it in a non-difficult, non-tedious way; 2) formalize it in a way that adheres closely to the English statement of the puzzle; 3) have an automated general-purpose commonsense reasoner that can accept that formalization and solve the puzzle quickly. In this paper, I present and discuss three formalizations that are less difficult and less tedious than the original. However, none satisfy all three requirements as well as might be desired, and there are a significant number of automated reasoners that cannot solve the puzzle using any of the formalizations. So the Jobs Puzzle remains an interesting challenge.

We present an approach to integrating rules and ontologies on the basis of the first-order stable model semantics proposed by Ferraris, Lee and Lifschitz. We show that some existing integration proposals can be uniformly reformulated in terms of the first-order stable model semantics. The reformulations are simpler than the original proposals in the sense that they do not refer to grounding.

We provide reformulations and generalizations of both the semantics of logic programs by Faber, Leone and Pfeifer and its extension to arbitrary propositional formulas by Truszczynski. Unlike the previous definitions, our generalizations refer neither to grounding nor to fixpoints, and apply to first-order formulas containing aggregate expressions. Similar to the first-order stable model semantics by Ferraris, Lee and Lifschitz, the reformulations presented here are based on syntactic transformations that are similar to circumscription. The reformulations provide useful insights into the FLP semantics and its relationship to circumscription and the first-order stable model semantics.

While much health data is available online, patients who are not technically astute may be unable to access it because they may not know the relevant resources, they may be reluctant to confront an unfamiliar interface, and they may not know how to compose an answer from information provided by multiple heterogeneous resources. We describe ongoing research in using natural English text queries and automated deduction to obtain answers based on multiple structured data sources in a specific subject domain. Each English query is transformed using natural language technology into an unambiguous logical form; this is submitted to a theorem prover that operates over an axiomatic theory of the subject domain. Symbols in the theory are linked to relations in external databases known to the system. An answer is obtained from the proof, along with an English language explanation of how the answer was obtained. Answers need not be present explicitly in any of the databases, but rather may be deduced or computed from the information they provide. Although English is highly ambiguous, the natural language technology is informed by subject domain knowledge, so that readings of the query that are syntactically plausible but semantically impossible are discarded. When a question is still ambiguous, the system can interrogate the patient to determine what meaning was intended. Additional queries can clarify earlier ones or ask questions referring to previously computed answers. We describe a prototype system, Quadri, which answers questions about HIV treatment using the Stanford HIV Drug Resistance Database and other resources. Natural language processing is provided by PARC’s Bridge, and the deductive mechanism is SRI’s SNARK theorem prover. We discuss some of the problems that must be faced to make this approach work, and some of our solutions.

This paper investigates the use of high-level action languages for representing and reasoning about commitments in mulit-agent domains. The paper introduces the language L mt with features motivates by the problem of representing commitments; in particular, it shows how L mt can handle both simple commitment actions and complex commitment protocols. The semantics of L mt provides a uniform solution to different problems in reasoning about commitments, e.g., the problem of (i) verifying whether an agent fails (or succeeds) to deliver on its commitments; (ii) identifying pending commitments; and (iii) suggesting ways to satisfy pending commitments.

In this paper we contribute to bridging the gap between human reasoning as studied in Cognitive Science and commonsense reasoning based on formal logics and formal theories. Stenning and van Lambalgen presented an approach to model human reasoning by means of logic programs. In this paper, we extend a refined version of their approach by abduction and demonstrate that this permits to adequately model various empiric results on the suppression task reported from Cognitive Science.

I begin by considering examples of practical reasoning. In the remainder of the paper, I try to say something about what Example 8. Playing soccer. Soccer is like table tennis, but a logical approach that begins to do justice to the subject with the added dimension of teamwork and the need to might be like. This task was selected as a benchmark problem in robotics, and has been extensively Example 1. Ordering a meal at a restaurant. Here, the problem is deciding what to eat and drink. Typing an email message, Even if the only relevant factors are price and preferences composing it as you go along, starts perhaps with a general about food, the number of possible combinations is very idea of what to say.

It has been argued that causal rules are necessary for representing both implicit side-effects of actions and action qualifications, and there have been a number different approaches for representing causal rules in the area of formal theories of actions. These different approaches in general agree on rules without cycles. However, they differ on causal rules with mutual cyclic dependencies, both in terms of how these rules are supposed to be represented and their semantics. In this paper we show that by adding one more minimization to Lin's circumscriptive causal theory in the situation calculus, we can have a uniform representation of causal rules including those with cyclic dependencies. We also demonstrate that sometimes causal rules can be compiled into logically equivalent (under a proposed semantics) successor state axioms even in the presence of cyclical dependencies between fluents.