Like Pearl’s System Z, c-representations provide a constructive approach to compute a ranking function from a conditional belief base from which further (conditional) beliefs can be derived, meeting major quality standards of nonmonotonic reasoning. This paper proposes a network-based structure for c-representations that allows for cutting down the complexity of reasoning significantly by decomposing the conditional belief base over a hypertree. We introduce c-LEG networks capturing the interactions among conditionals on a syntactical basis in full compatibility with the semantics of c-representations. This allows for reasoning in much smaller local contexts while still complying with the global information provided by the full conditional belief base. Moreover, we generalize the so-called safety property, which was recently presented in the context of conditional syntax splitting, to ensure that local c-representations of subbases over the hyperedges can be merged to yield global c-representations of the full conditional belief base. This allows for computing global c-representations step by step in local contexts, following the structure of the hypertree.

Splitting techniques in knowledge representation help focus on relevant parts of a belief base and reduce the complexity of reasoning generally. In this paper, we propose a generalization of safe conditional syntax splittings that broadens the applicability of splitting postulates for inductive inference from belief bases. In contrast to safe conditional syntax splitting, our generalized notion supports syntax splittings of a belief base ∆ where the subbases of ∆ may share atoms and nontrivial conditionals. We illustrate how this new notion overcomes limitations of previous splitting concepts, and we identify genuine splittings, separating them from simple splittings that do not provide benefits for inductive inference from ∆. We introduce adjusted inference postulates based on our generalization of conditional syntax splitting. We evaluate several inductive inference operators with respect to these postulates, and show that generalized safe conditional syntax splitting is a strictly stronger requirement for inductive inference operators, covering more syntax splitting applications.

The concept of conditional syntax splitting for inductive inference from conditional belief bases has been proposed as a generalization of syntax splitting which also covers cases where the conditionals in the subbases share some atoms. p-Entailment and system Z fail to satisfy conditional syntax splitting, and up to now, only two inductive inference operators, lexicographic inference and system W, have been shown to satisfy this property. In this paper, we introduce the concept of conditional semantic splitting. We show that c-representations satisfy a core postulate relating conditional splittings on the syntax and the semantic level. Based on these findings, we investigate conditional syntax splitting for nonmonotonic inference with c-representations. Regarding single c-representations, we utilize the concept of selection strategies, and show that a straightforward property of the selection strategy leads to inference operators satisfying conditional syntax splittings. Furthermore, we show that c-inference taking all c-representations of a belief base into account also fully complies with conditional syntax splitting.

Total preorders and Spohn’s ranking functions are most popular semantic structures in nonmonotonic reasoning and belief revision. Each ranking function uniquely induces a total preorder, while each total preorder corresponds to infinitely many ranking functions because of the empty layers that ranking functions may have. In this paper, we adopt a dynamic perspective and investigate the role of empty layers in belief revision scenarios. We strengthen the notion of (inferential) equivalence of ranking functions by introducing revision equivalence which postulates the equivalence of ranking functions after (most general) revision operations. Moreover, we single out so-called linearly equivalent ranking functions as prototypes of ranking functions with regularly inserted empty layers. Such ranking functions are most suitable to provide an invariance property for revision equivalence which claims that linear equivalence should be preserved. We show that strategic c-revisions ensure (conditional) revision equivalence of linearly equivalent ranking functions if the strategies are adequately chosen, whereas the Darwiche-Pearl postulates for iterated revision alone are not enough to guarantee revision equivalence of ranking functions. We evaluate various other iterated revision approaches from the literature with respect to revision equivalence and preserving linear equivalence under revision. Furthermore, we present an approach to defining equivalence preserving revision operators for ranking functions from revision operators for total preorders.

A qualitative conditional “If A then usually B” establishes a plausible connection between the antecedent A and the consequent B. As a semantics for conditional knowledge bases containing such conditionals, ranking functions order possible worlds by mapping them to a degree of plausibility. c-Representations are special ranking functions that are obtained by assigning individual integer impacts to the conditionals in a knowledge base R and by defining the rank of each possible world as the sum of these impacts of falsified conditionals. c-Inference is the nonmonotonic inference relation taking all c-representations of a given knowledge base R into account. In this paper, we show how c-inference can be realized as a satisfiability modulo theories problem (SMT), which allows an implementation by an appropriate SMT solver . Moreover, we show that this leads to the first implementation fully realizing c-inference because it does not require a predefined upper limit for the impacts assigned to the conditionals. We develop a transformation of the constraint satisfaction problem characterizing c-inference into a solvable-equivalent SMT problem, prove its correctness, and illustrate it by a running example. Furthermore, we provide a corresponding implementation using the SMT solver Z3. We develop and implement a randomized generation scheme for knowledge bases and queries, and evaluate our SMT-based implementation of c-inference with respect to such randomly generated knowledge bases. Our evaluation demonstrates the feasibility of our approach as well as the superiority in comparison to former implementations of c-inference.

In this article, we investigate approximations of the inductive inference operator system W that has been shown to exhibit desirable inference properties and to extend both system Z, and thus rational closure, and c-inference. For versions of these inference operators that are extended to also cover inference from belief bases that are only weakly consistent, we first show that extended system Z and extended c-inference are captured by extended system W. Then we introduce general functions for generating inductive inference operators: the combination of two inductive inference operators by union, and the completion of an inductive inference operator by an arbitrary set of axioms. We construct the least inductive inference operator extending system Z and c-inference that is closed under system P and show that it is still strictly extended by extended system W. Furthermore, we introduce an inductive inference operator that strictly extends extended system W and that is strictly extended by lexicographic inference. This leads to a comprehensive map of inference relations between rational closure and extended c-inference on the one side and lexicographic inference on the other side with extended system W and its approximations at its centre, where all relationships also hold for the unextended versions. • Introducing the union of inductive inference operators and the closure of inductive inference under a set of postulates. • Showing that system W, extended to cover weakly consistent belief bases, captures extended system Z and extended c-Inference. • Showing that extended system W is captured by adapted lexicographic inference. • Introducing the minimal inductive inference operator extending c-inference and system Z as approximation of system W. • Development of a comprehensive map of inductive inference operators that approximate (extended) system W.

Syntax splitting is a property of inductive inference operators that ensures we can restrict our attention to parts of the conditional belief base that share atoms with a given query. To apply syntax splitting, a conditional belief base needs to consist of syntactically disjoint conditionals. This requirement is often too strong in practice, as conditionals might share atoms. In this paper we introduce the concept of conditional syntax splitting, inspired by the notion of conditional independence as known from probability theory. We show that lexicographic inference and system W satisfy conditional syntax splitting, and connect conditional syntax splitting to several known properties from the literature on non-monotonic reasoning, including the drowning effect.

The notion of syntax splitting was initially introduced by Parikh for belief sets, and one key observation is that every belief set has a unique finest syntax splitting, i.e., a syntax splitting that refines every other syntax splitting of that belief set. Later, the notion of syntax splitting was extended to ranking functions and total preorders on worlds (TPOs), which are two common models for belief states in the context of iterated belief revision. In this paper, we prove that ranking functions also have unique finest syntax splittings, i.e., every ranking function has a syntax splitting that refines all other syntax splittings of that ranking function. Using this, we can show that the syntax splittings of a ranking function κ are exactly the coarsenings of the finest splitting of κ. For TPOs we show that, in contrast to ranking functions, the coarsening of a syntax splitting of a TPO ⪯ is not necessarily a syntax splitting of ⪯. Despite that we can prove that every TPO has a unique finest syntax splitting that refines all other syntax splittings of that TPO.

Conditional independence is a crucial concept for efficient probabilistic reasoning. For symbolic and qualitative reasoning, however, it has played only a minor role. Recently, Lynn, Delgrande, and Peppas have considered conditional independence in terms of syntactic multivalued dependencies. In this paper, we define conditional independence as a semantic property of epistemic states and present axioms for iterated belief revision operators to obey conditional independence in general. We show that c-revisions for ranking functions satisfy these axioms, and exploit the relevance of these results for iterated belief revision in general.

InfOCF-Web provides implementations of system P and system Z inference, and of inference relations based on c-representation with respect to various inference modes and different classes of minimal models. It has an easy-to-use online interface for computing ranking models of a conditional knowledge R, and for answering queries and comparing inference results of nonmonotonic inference relations induced by R.

According to Boutillier, Darwiche, Pearl and others, principles for iterated revision can be characterised in terms of changing beliefs about conditionals. For iterated contraction a similar formulation is not known. This is especially because for iterated belief change the connection between revision and contraction via the Levi and Harper identity is not straightforward, and therefore, characterisation results do not transfer easily between iterated revision and contraction. In this article, we develop an axiomatisation of iterated contraction in terms of changing conditional beliefs. We prove that the new set of postulates conforms semantically to the class of operators like the ones given by Konieczny and Pino P\'erez for iterated contraction.

Parikh developed the notion of syntax splitting to describe belief sets with independent parts. He also formulated a postulate demanding that belief revisions respect syntax splittings in belief sets. The concept of syntax splitting was later transferred to epistemic states with total preorders and ranking functions by Kern-Isberner and Brewka along with corresponding postulates for belief revisions. Besides revision, contraction is also a central operation in the field of general belief change. In this paper, we analyse belief contractions with respect to syntax splitting. Based on the work on syntax splitting for revision, we develop syntax splitting postulates for contractions on ranking functions, on epistemic states with total preorder, and on belief sets. Finally, we evaluate different contractions from the literature, namely moderate contraction, natural contraction, lexicographic contraction, and c-contractions with respect to the newly developed contraction postulates.

Syntax splitting, first introduced by Parikh in 1999, is a natural and desirable property of KR systems. Syntax splitting combines two aspects: it requires that the outcome of a certain epistemic operation should only depend on relevant parts of the underlying knowledge base, where relevance is given a syntactic interpretation (relevance). It also requires that strengthening antecedents by irrelevant information should have no influence on the obtained conclusions (independence). In the context of belief revision the study of syntax splitting already proved useful and led to numerous new insights. In this paper we analyse syntax splitting in a different setting, namely nonmonotonic reasoning based on conditional knowledge bases. More precisely, we analyse inductive inference operators which, like system P, system Z, or the more recent c-inference, generate an inference relation from a conditional knowledge base. We axiomatize the two aforementioned aspects of syntax splitting, relevance and independence, as properties of such inductive inference operators. Our main results show that system P and system Z, whilst satisfying relevance, fail to satisfy independence. C-inference, in contrast, turns out to satisfy both relevance and independence and thus fully complies with syntax splitting.

In an ongoing project aiming at a comprehensive AI-based tool to support clinical decisions in medical cancer therapy, the ontology OCTA is being developed. Its purpose is to provide general knowledge about active ingredients, therapy regimens, etc. that can be used by such a clinical decision support system. In this paper, we present a new extension of OCTA modelling co-medication and drug interactions, enabling the answering of queries relevant for medical decision making dealing with these aspects.

While the axiomatic system P is an important standard for plausible nonmonotonic reasoning, inference relations obtained from system Z or from c-representations have been designed which go beyond system P. In this paper, we propose the new concept of weakly skeptical inference that properly extends the recently introduced skeptical c-inference, but avoids disadvantages of a too liberal credulous inference. We extend the concepts of skeptical, weakly skeptical, and credulous c-inference by taking preferred models obtained from different minimality criteria into account. We illustrate the usefulness of the obtained inference relations, show that they fulfill various desirable properties, and elaborate on their interrelationships.

Dealing with uncertainty that is inherently present in any medical domain, is one of the major challenges when designing a medical decision support system. We demonstrate how probabilistic logic can be used to design medical knowledge bases at the example of analysing clinical brain tumor data. We use MECoRe, a system implementing probabilistic conditional logic, to create a knowledge base BT that contains medical knowledge originating from both statistical data as well as from medical experts. Any incomplete or unspecified knowledge is completed by MECoRe in an information-theoretically optimal way by employing the principle of maximum entropy. BT is evaluated with respect to a series of queries regarding diagnosis and prognosis, using a real documented patient case.

Large-scale neuroimaging databases provide a rich fundus of functional neuroimaging experiments exhibiting maximum activation coordinates for specific task conditions. Aiming to explore major neuronal networks of the human brain, we developed a meta-analytic pattern-mining approach which combines Gaussian mixture modeling with the Apriori algorithm to identify frequent activation patterns within these databases. The approach has been implemented in the PaMiNI (Pattern Mining in NeuroImaging) system, providing manifold facilities for the finding, inspection, and analysis of relevant patterns. After briefly sketching the background of PaMiNI, we give an overview of the system and describe its architecture. Using an example application, a system walkthrough illustrates how PaMiNI can be used for the discovery of networks comprising functionally connected brain regions.

Legal reasoning is one of the most obvious application areas for computational models of argumentation as the exchange of arguments and counterarguments is the established means for making decisions in law. In this paper we employ Defeasible Logic Programming (DeLP) for representing legal cases and for giving decision-support, exemplary for private law. We give a formalization of legal provisions that can be used easily by judges for supporting their decision process and present a working system that resembles the decision-making in legal reasoning, in particular, with respect to the burden of proof.

Abstract We provide a mathematical specification of an extension of Warren's Abstract Machine (WAM) for executing Prolog to type-constraint logic programming and prove its correctness. Our aim is to provide a full specification and correctness proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L. In this paper, while leaving the details of the PAM's type constraint representation and solving facilities to a sequel to this work, we keep the notion of types and dynamic type constraints abstract to allow applications to different constraint formalisms like Prolog III or CLP(R). This generality permits us to introduce modular extensions of Börger's and Rosenzweig's formal derivation of the WAM. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND/OR structure that are derived from Börger's and Rosenzweig's corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level, and for each refinement step a correctness proof is given. Thus, we obtain the theorem that for every such abstract type-constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct.

Abstract We refine the mathematical specification of a WAM extension to typeconstraint logic programming given in [BeB96]. We provide a full specification and correctness proof of the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L, by refining the abstract type constraints used in [BeB96] to the polymorphic order-sorted types of PROTOS-L. This allows us to develop a detailed and mathematically precise account of the PAM's compiled type constraint representation and solving facilities, and to extend the correctness theorem to compilation on the fully specified PAM.

The logic-based knowledge representation language L/sub LILOG/, which is used to represent both the semantic background knowledge as well as the information extracted from German texts within the LILOG project, is discussed. L/sub LILOG/ integrates frame-like features-value descriptions used in computational linguistics into an order-sorted predicated logic framework. The basis design principles of L/sub LILOG/ and examples of how L/sub LILOG/ is used to model real world knowledge are presented. The implementation of the first LILOG prototype is described. A formal semantics definition is provided.>