A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.

This paper gives a new, proof-theoretic explanation of partial-order reasoning about time in a nonmonotonic theory of action. The explanation relies on the technique of lifting ground proof systems to compute results using variables and unification. The ground theory uses argumentation in modal logic for sound and complete reasoning about specifications whose semantics follows Gelfond and Lifschitz’s language. The proof theory of modal logic A represents inertia by rules that can be instantiated by sequences of time steps or events. Lifting (...) such rules introduces string variables and associates each proof with a set of string equations; these equations are equivalent to a set of partial-order tree-constraints that can be solved efficiently. The defeasible occlusion of inertia likewise imposes partial-order constraints in the lifted system. By deriving an auxiliary partial order representation of action from the underlying logic, not the input formulas or proofs found, this paper strengthens the connection between practical planners and formal theories of action. Moreover, the general correctness of the theory of action justifies partial-order representations not only for forward reasoning from a completely specified start state, but also for explanatory reasoning and for reasoning by cases. (shrink)

cal practice: the enterprise of specifying information about the world for use in computer systems. Knowledge representation as a field also encompasses conceptual results that call practitioners’ attention to important truths about the world, mathematical results that allow practitioners to make these truths precise, and computational results that put these truths to work. This chapter surveys this practice and its results, as it applies to the interpretation of natural language utterances in implemented natural language processing systems. For a broader perspective (...) on such technical practice, in all its strengths and weaknesses, see (Agre 1997). Knowledge representation offers a powerful general tool for the science of language. Computational logic, a prototypical formalism for representing knowledge about the world, is also the model for the level of logical form that linguists use to characterize the grammar of meaning (Larson and Segal 1995). And researchers from (Schank and Abelson 1977) to (Shieber 1993) and (Bos to appear) have relied crucially on such representations, and the inference methods associated with them, in articulating accounts of semantic relations in language, such as synonymy, entailment, informativeness and contradiction. The new textbooks (Blackburn and Bos 2002a, Blackburn and Bos 2002b) provide an excellent grounding in this research, and demonstrate how deeply computational ideas from knowledge representation can inform pure linguistic study. In this short chapter, I must leave much of.. (shrink)

. The current literature in the Artificial Intelligence and Law field reveals uncertainty concerning the potential role of deontic logic in legal knowledge representation. For instance, the Logic Programming Group at Imperial College has shown that a good deal can be achieved in this area in the absence of explicit representation of the deontic notions. This paper argues that some rather ordinary parts of the law contain structures which, if they are to be represented in logic, will call for use (...) of a reasonably sophisticated deontic logic. (shrink)

I show how a conversational process that takes simple, intuitively meaningful steps may be understood as a sophisticated computation that derives the richly detailed, complex representations implicit in our knowledge of language. To develop the account, I argue that natural language is structured in a way that lets us formalize grammatical knowledge precisely in terms of rich primitives of interpretation. Primitives of interpretation can be correctly viewed intentionally, as explanations of our choices of linguistic actions; the model therefore fits our (...) intuitions about meaning in conversation. Nevertheless, interpretations for complex utterances can be built from these primitives by simple operations of grammatical derivation. In bridging analyses of meaning at semantic and symbol‐processing levels, this account underscores the fundamental place for computation in the cognitive science of language use. (shrink)