We present a weighted algebraic non-monotonic logic we refer to as LogAG for reasoning with uncertain beliefs. In LogAG, the classical logical formulas could be associated with ordered grades representing measures of uncertainty. The revision of beliefs in LogAG, when contradictions arise, is done according to the grades of the contradictory propositions. Throughout the paper, we present the syntax and semantics of LogAG, extending the classical notion of logical consequence to handle graded propositions. A proof theory for LogAG is thoroughly described, discussing its soundness and completeness. Finally, we demonstrate the utility of LogAG in non-monotonic reasoning and in reasoning about information provided by a chain of sources of varying degrees of trust.
Most of the commonsense reasoning we perform in our everyday lives typically involves uncertain, possibly contradicting, beliefs. Consequently, any intelligent agent emulating human reasoning must be able to handle uncertain knowledge in a way that facilitates drawing reasonable conclusions, and resolve contradictions when they arise. Tremendous research effort has been made over the years to attempt to understand and model uncertain reasoning [Halpern, 2017]. The work presented in this paper is one such attempt.
In this paper, we extend a logic we refer to as LogAG for reasoning with uncertain beliefs by presenting its proof theory. The syntax and semantics of LogAG is thoroughly described in [Ehab, 2016; Ismail and Ehab, 2015]. “Log” stands for logic, “A” for algebraic, and “G” for grades. In LogAG, a classical logical formula could be associated with a grade representing a measure of its uncertainty. Non-graded formulas are taken to be certain. In this way, LogAG is a logic for reasoning about graded propositions. LogAG is algebraic in that it is a language of only terms, some of which denote propositions. Both propositions and their grades are taken as individuals in the LogAG ontology. Thus, the language includes terms denoting graded propositions, grades of propositions, grading propositions, and graded grading propositions in an arbitrary compositional structure. While some multimodal logics such as [Demolombe and Liau, 2001; Milosˇevic´ and Ognjanovic´, 2012] may be used to express graded grading propositions too, unlike LogAG, the grades themselves are embedded in the modal operators and are not amenable to reasoning and quantification. We will show throughout this paper that this is not the case with LogAG. This makes LogAG a quite expressive language that is still intuitive and very similar in syntax to first-order logic.
While most of the weighted logics we are aware of employ non-classical modal logic semantics by assigning grades to possible worlds [Dubois et al., 2014], LogAG is a nonmodal logic with classical notions of worlds and truth values. This is not to say that LogAG is a classical logic, but it is closer in spirit to classical non-monotonic logics such as default logic [Reiter, 1980] and circumscription [McCarthy, 1980]. Following these formalisms, LogAG assumes a classical notion of logical consequence on top of which a more restrictive, non-classical relation is defined selecting only a subset of the classical models. In defining this relation we take the algebraic, rather than the modal, route.
In Sections 2 and 3, the syntax and semantics of LogAG are reviewed. In Section 4, we show that LogAG is a stable and well-behaved non-monotonic logic by discussing some of the properties of the extended logical consequence relation. Next, we present in Section 5 the LogAG proof theory discussing its soundness and completeness. Finally, we show running examples from an implementation of LogAG in Section 6 demonstrating the utility of LogAG in non-monotonic reasoning and in reasoning about information provided by a chain of sources of varying degrees of trust. 2
LogAG consists of algebraically constructed terms from function symbols. There are no sentences in LogAG; instead, we use terms of a distinguished syntactic type to denote propositions. Propositions are included as first-class individuals in the LogAG ontology and are structured in a Boolean algebra giving us all standard truth conditions and classical notions of consequence and validity. The inclusion of propositions in the ontology, though non-standard, has been suggested by several authors [Church, 1950; Bealer, 1979; Parsons, 1993; Shapiro, 1993]. Additionally, grades are introduced as first-class individuals in the ontology. As a result, propositions about graded propositions can be constructed, which are themselves recursively gradable.
A LogAG language is a many-sorted language composed of a set of terms partitioned into three base sorts: P is a set of terms denoting propositions, D is a set of terms denoting grades, and I is a set of terms denoting anything else. A LogAG alphabet includes a non-empty, countable set of constant and function symbols each having a syntactic sort from the set = f P ; D; I g [ f 1 ! 2 j 1 2 f P ; D; I gg and 2 2 g of syntactic sorts. Intuitively, 1 ! 2 is the syntactic sort of function symbols that take a single argument of sort P , D, or I and produce a functional term of sort 2. (Given the restriction of the first argument of function symbols to base sorts, LogAG is, in a sense, a first-order language.) In addition, an alphabet includes a countably infinite set of variables of the three base sorts; a set of syncategorematic symbols including the comma, various matching pairs of brackets and parentheses, and the symbol 8; and a set of logical symbols defined as the union of the following sets: : ! P P , f ; = D P P . 1 P , f^; _g P ! P , and fGg
! ! D P ! ! D ! f:g g 3
We will begin this section by presenting the interpretation of the LogAG syntactic structures along with the algebraic definition of logical consequence. Next, we will thoroughly describe our proposed extension of logical consequence to address uncertain reasoning with graded propositions. Throughout this section, only sketches of the proofs will be shown for space limitations. 3.1
A key element of defining the semantics of LogAG is the notion of a LogAG structure.
S = hD; A; g; <; ei, where
D, the domain of discourse, is a set with two disjoint, non-empty, countable subsets: P denoting a set of propositional terms, and G denoting a set of grading terms.
A = hP; +; ; ; ?; >i is a complete, non-degenerate
g : P G ! P is a grading function. <: G G ! P is an ordering function. e : G G ! f?; >g is an equality function, where for every g1; g2 2 G: e(g1; g2) = > if g1 = g2, and e(g1; g2) = ? otherwise.
The three blocks of the domain of discourse P; G; and P [ G stand in correspondence to the three base syntactic sorts P ; D; and I respectively. The set of propositions P is interpreted by a complete, non-degenerate Boolean algebra A. g is a function that maps a proposition p 2 P and a grade g 2 G to the proposition that the grade of p is g. By not imposing any further restrictions on g, we allow any reasonable 1Terms involving ), ,, and 9 can always be expressed in terms of the above logical operators and 8. notion of grading. < is an ordering function on the grades in G. It maps two grades g1 and g2 to the proposition that g1 is less than g2. Some restrictions are imposed on < as mentioned in [Ismail and Ehab, 2015] to give rise to an irreflexive linear order on G which is serial in both directions.
A valuation V of a LogAG language is a triple hS; Vf ; Vxi, where S is a LogAG structure, Vf is a function that assigns to each function symbol an appropriate function on D, and Vx is a function mapping each variable to a corresponding element of the appropriate block of D. An interpretation of LogAG terms is given by a function [[ ]]V . Figure 1 summarizes the operation of [[ ]]V . The formal definition of [[ ]]V can be found in [Ismail and Ehab, 2015].
We define logical consequence using the familiar notion of filters from Boolean algebra [Sankappanavar and Burris, 1981]. A propositional term is a logical consequence of a set of propositional terms if it is a member of the filter of the interpretation of , denoted F ([[ ]]V ).
Definition 3.2. Let L be a LogAG language. For every 2
j= , if, for every L-valuation V, [[ ]]V 2 F ([[ ]]V ) where [[ ]]V = Y [[ ]]V :
2 3.2
The definition of logical consequence presented in the previous section cannot address uncertain reasoning with graded propositions. To see that, consider an agent reasoning with a set of propositional terms Q as shown in Figure 2. It would make sense for the agent to be able to conclude p even if p is uncertain (and, hence, graded) since it has no reason to believe :p. The filter F (Q), however, contains the classical logical consequences of Q, but will never contain p. For this reason, we extend our classical notion of filters into a more liberal notion of graded filters to enable the agent to conclude, in addition to the classical logical consequences of Q, propositions that are graded in Q or follow from graded propositions in Q. This should be done without introducing inconsistencies. Due to nested grading, graded filters come in degrees depending on the depth of nesting of the admitted graded propositions. In Figure 2, F 1(Q) is the graded filter of degree 1. F 1(Q) contains everything in F (Q) in addition to the nested graded propositions at depth 1, p and g(:q; d1). q and r are also admitted to F 1(Q) since they follow classically from fp; p ) qg and fp; p ) rg respectively. To compute the graded filter of degree 2, F 2(Q), we take everything in F 1(Q) and try to add the graded proposition :q at depth 2. The problem is, once we do that, we have a contradiction with q. To resolve the contradiction, we admit to F 2(Q) either p (and consequently q and r) or :q. In deciding which of p and :q to kick out we will allude to their grades. The grade of p is d1, and :q is graded in a grading chain containing d1 and d2. To get a fused grade for :q, we will combine both d1 and d2. If d1 is less than the fused grade of :q, p will not be admitted to the graded filter, together with its consequences q and r. Otherwise, :q will not be admitted, and p, q, and r will remain. If we try to compute F 3(Q), we get everything in F 2(Q) reaching a fixed point. In general, the elements of F i(Q) will be referred to as the graded consequences at depth i. In what follows, graded filters will be formally defined.
The key to defining graded filters is the intuition that the set of consequences of a proposition set Q may be further enriched by telescoping Q and accepting some of the propositions graded therein. For this, we need to define (i) the process of telescoping, which is a step-wise process that considers propositions at increasing grading depths, and (ii) a criterion for accepting graded propositions which, as mentioned before, depends on the grades of said propositions. Since the nesting of grading chains is permissible in LogAG, it is necessary to compute the fused grade of a graded proposition p in a chain C to decide whether it will be accepted or not. The fusion of grades in a chain is done according to an operator . Further, since a graded proposition p might be graded by more than one grading chain, we define the notion of the fused grade of p across all the chains grading it by an operator .
and fan-out-bounded P 2. A telescoping structure for S is a quadruple T = hT ; O; ; i, where
P, referred to as the top theory; T
: Si1=1 Gi ! G; and : Si1=1 Gi ! G.
Recasting the familiar notion of a kernel of a belief base [Hansson, 1994] into the context of LogAG structures, we say that a ?-kernel of Q P is a subset-minimal inconsistent set X Q such that F (E(F (X ))) is improper (= P) 2P is depth-bounded if every grading chain has at most d distinct grading propositions and is fan-out-bounded if every grading proposition grades at most fout propositions [Ismail and Ehab, 2015].
Q given T if 1. p 2 F (T ); or
P. We say that p is supported in in the filter of X . Let Q ? be the set of Q kernels that entail ?. A proposition p 2 X survives X in T if p is not the weakest proposition (with the least grade) in X . In what follows, the fused grade of a proposition p in Q P according to a telescoping structure T will be referred to as fT(p; Q).
hT ; O; ; i and a fan-in-bounded 3 Q P, if X then p 2 X survives X given T if = Q, 1. p is ungraded in Q; or 2. there is some ungraded q 2 X such that q 2= F (T ); or 3. there is some graded q 2 X such that q 2= F (T ) and (fT(q; Q) < fT(p; Q)) 2 O.
The set of kernel survivors of Q given T is the set (Q; T) = fp 2 Qj if p 2 X 2 Q given Tg.
? then p survives X
The notion of a proposition p being supported in Q is defined as follows.
2. there is a grading chain hq0; q1; : : : ; qni of p in Q with q0 2 F (R) where every member of R is supported in Q. The set of propositions supported in Q given T is denoted by &(Q; T ).
Observation 1. If F (T ) is proper, then F (&( (Q; T); T )) is proper.
Proof. If F (&( (Q; T); T )) is not proper, then &( (Q; T); T ) has at least one kernel X 2 Q ?. According to Definitions 3.4 and 3.5, this can only happen if X T . Thus, F (T ) is proper.
In what follows, the graded propositions at depth 1 of the filter of Q will be denoted as E1(F (Q)). The T-induced telescoping of Q is defined as the set of propositions supported given T in the set of kernel survivors of E1(F (Q)). Definition 3.6. Let T be a telescoping structure for S, If Q P such that E1(F (Q)) is fan-in-bounded, then the T-induced telescoping of Q is given by
T(Q) = &( (E1(F (Q)); T); T ):
If F (Q) has finitely-many grading propositions, then T(Q) is defined, for every telescoping structure T. Hence, provided that the right-hand side is defined, let n T (Q) =
Q if n = 0
T( Tn 1(Q)) otherwise Finally, a graded filter of a top theory T , denoted F n(T), is defined as the filter of the T-induced telescoping of T of degree n.4
3Q is fan-in-bounded if every graded proposition is graded by at most fin grading propositions.
4In general, even with a finite and fan-in-bounded T , the existence of a fixed-point for graded filters is not secured as discussed in [Ismail and Ehab, 2015].
Example 3.1 in Figure 3 illustrates the construction of graded filters.
Example 3.1 Consider Q = f p + q; p + r; g(p; 2); g(g( q; 2); 3)g and T = hQ; O; ; i where = max, and = mean.
T0 = Q T1 = T( T0 ) = &( (E1(F (Q)); T); T ) F (Q) = Q [ f p + q:g(p; 2); g(g( q; 2); 3) + g(p; 2); ::::g E1(F (Q) = F (Q) [ fp; g( q; 2)g (E1(F (Q); T) = E1(F (Q) T1 = (E1(F (Q); T) = &( (E1(F (Q); T); Q) F1(T) = F ( T1 ) Upon telescoping to degree 1, there are no contradictions in E1(F (Q)) (no X E1(F (Q)). Hence, everything in E1(F (Q)) survives telescoping and is supported.
T2 =
T( T1 ) E(1E(F1((FT1( )T)1 )=);FT() =T1 )F[( fT1 )qg
fpg T2 = &( (E1(F ( T1 )); T); Q) = (E1(F ( T1 )); T) fq; rg F2(T) = F ( T2 ) Upon telescoping to degree 2, there are two ? kernels fq; qg and fp; p + q; qg. q survives the first kernel as it is not graded in Q.
q survives the first kernel as well as it is the only graded proposition in the kernel with another member q 2= F (Q). p does not survive the second kernel as the kernel contains another graded proposition q and the grade of p (2) is less than the fused grade of q (2.5). Accordingly, q and r lose their support and are not supported in the set of kernel survivors. The graded filter of degree 2 does not contain p, q or r.
T3 = T( T2 ) T3 = &( (E1(F ( T2 )); T); Q) = (E1(F ( T2 )); T) F3(T) = F ( T3 ) = F2(T) reaching a fixed point.
We use graded filters to define graded consequence as follows. Given a LogAG theory T P and a valuation V = hS; Vf ; Vxi, let V(T) = f[[p]]V j p 2 Tg. Further, for a LogAG structure S, an S grading canon is a triple C = h ; ; ni where n 2 N and and are as indicated in Definition 3.3.
Definition 3.7. Let T be a LogAG theory and V = hS; Vf ; Vxi a valuation, where S has a set P which is depthand fan-out-bounded, for some LogAG language L. For every p 2 P and S grading canon C = h ; ; ni, p is a graded consequence of T with respect to C, denoted T j'C p, if F n(T) is defined and [[p]]V 2 F n(T), for every telescoping structure T = hV(T); O; ; i for S, where O extends F (V(T) \ Range(<)). (An ultrafilter U extends a filter F , if F U .)
It is worth noting that j'C reduces to j= if n = 0 or if F (E(V(T))) does not contain any grading propositions. However, unlike j=, j'C is non-monotonic in general. 4
One way of evaluating non-monotonic formalisms in
literature
Since according to Definition 3.7 the graded consequence relation of LogAG is based on graded filters, we first present a property of graded filters. The following theorem states that graded filters of a consistent theory are always consistent. This implies that reasoning in LogAG is consistency preserving.
Theorem 4.1. If T is a telescoping structure where F (T ) is proper, then, if defined, F n(T) is proper, for every n 2 N. Proof. For n = 0, the statement is trivial, since F 0(T) = F (T ). Otherwise, the statement follows directly from Observation 1 since, by the definition of graded filters, F k+1(T) = F (K), for some K (E1(F k(T)); T).
A widely accepted view of Gabbay [Gabbay, 1985] for assessing whether a formalism is considered to be a reasonable non-monotonic logic asserts that reasoning the formalism’s logical consequence relation should observe reflexivity, cut, and cautious monotony.
The following lemma will be useful in the proof of the following theorem.
Lemma 4.1. For any proposition p, let T1 = hT ; O; ; i, T2 = hT [ fpg; O; ; i, and i 2 N. If F i(T1) is a fixed point where p 2 F i(T1), then there is some j 2 N such that F j (T2) is a fixed point and F i(T1) = F j (T2).
Theorem 4.2. For any proposition p, let T1 = hTn;(OT;1) ;andi and T2 = hT [ fpg; O; ; i. Further, let F F m(T2) be fixed points where n; m 2 N. The graded consequence relation of LogAG defined in terms of graded filters observes the following extended versions of reflexivity, cut, and cautious monotony.
1. Reflexivity: If p 2 T , then p 2 F n(T1). 2. Cut: If p 2 F n(T1) and q 2 F m(T2),
then q 2 F n(T1). 3. Cautious Monotony: If p 2 F n(T1) and q 2 F n(T1), then q 2 F m(T2).
Proof. Reflexivity follows directly from Clause 1 in Definition 3.5 and the definition of graded filters.
If q 2 F m(T2), then according to Lemma 4.1 it must be the case that q 2 F n(T1). Accordingly, the graded consequence of LogAG relation observes cut.
Similarly, if p 2 F n(T1) and q 2 F n(T1), then it follow from Lemma 4.1 that q 2 F m(T2). Accordingly, the graded consequence relation of LogAG observes cautious monotony. 5
In order to compute the graded filter of degree n, all ?kernels are to be computed, which is undecidable for firstorder logic according to Church’s Theorem [Bo¨rger et al., 2001; Raatikainen, 2015]. For this reason, the proposed proof theory takes an alternative approach. A set of supports is kept track of for every proposition enabling the computation of some of the ?-kernels. Further, the natural deduction rules of classical logic are modified to update the supports of the inferred propositions, and a special derivation rule of telescoping is added. This special rule of inference will extract any graded proposition in any grading chain. It is worth noting that this is different from our semantic notion of telescoping presented in the last section. As will be shown, this new derivation rule can introduce contradictions. Hence, a way of handling said contradictions is proposed.
We refer to a belief space as a context. To accommodate reasoning with graded propositions, a context is defined as a pair C = hHS; T Si where HS is a set of hypotheses (facts), and T S is a set of telescoped (graded) propositions. The context where the current inference is done is referred to as the current context.
Each propositional term p is associated with a set of supports, where each support corresponds to a unique derivation of p. We extend the structure of a support suggested in [Martins and Shapiro, 1988] to include graded supports. Definition 5.1. A support of a proposition p is a pair s = hO; T i where O [ T j= p. O will be referred to as the origin set, and T will be referred to as the telescoped supports set.
To accommodate the supports of propositions, a supported knowledge base is defined as follows:
hP; S; Gi where:
P P .
S is a function mapping each propositional term p 2 P to a set of supports of p.
G is a function mapping each propositional term p 2 P to a set of sequences of grade terms of the syntactic sort
In what follows, we will assume that all grade terms appearing in P are numerals. Each sequence in G(p) contains the grades associated with p in a particular chain. This will facilitate computing the fused grade of p. Given a grading canon C = h ; ; ni the fused grade of a proposition p 2 P is defined as follows.
Definition 5.3. Let KB = hP; S; Gi, for any proposition p 2 P, the fused grade of p is defined as f (p) = length(G(p))) for every Gi 2 L(f (Gi)i=1 length(Gi) n.
At any point of time, not all propositional terms p 2 P will be believed in a context.
Definition 5.4. Let KB = hP; S; Gi be a supported knowledge base. A propositional term p 2 P is said to be asserted (believed) in a context C = hHS; T Si if there is a support hO; T i 2 S(p) where O HS and T T S.
The proposed proof theory is similar in spirit to the Fitchstyle natural deduction rules. However, it does not enforce specific inference rules for the classical rules of inference (the introduction and elimination rules for :; ); ^; _; and 8) for the sake of generality. Any inference rule I will be applied to a supported KB, and will result in an updated supported KB (I(KB = hP; S; Gi) = KB0 = hP0; S0; G0i). We can think of any classical inference rule as one of the following two types 5:
5An example set of classical Fitch-style inference rules is presented in [Ehab, 2016].
In addition to the classical rules of inference, the proposed proof theory adds a special inference rule of telescoping (T el). T el will extract a graded proposition from a grading proposition, and result in a new updated supported knowledge base. T el will also change the T S set of the current context. The T S set of the current context will contain the propositional terms telescoped using the telescoping rule of inference from grading propositional terms in HS, or derivable from HS using any of the inference rules. T el is defined as follows:
If G(p; g) 2 P, the updated knowledge base KB0 = hP0; S0; T0i where P0 = P [ fpg, S0(p) = S(p) [ T elSup(p), and G0(p) = G(p) [ T elGrades(p). T elSup(p) = fhO; T [ fpgi j hO; T i 2 S(p)g and T elGrade(p) = fGi hgi j Gi 2 G(G(p; g)) and denotes sequence concatenationg. The new current context is C = hHS; T S [ fpgi:
A support for a propositional term p, s = hO; T i 2 S(p), is a hypothesis support if O = fpg. s is a telescoped support if p 2 T . Otherwise, s is a derived support. 5.3
In the sequel, we assume a non-contradictory KB such that any contradictions are only derived by applying the rule of telescoping, or by applying any sequence of inference rules on a minimal set containing a telescoped proposition. Once p and :p are derived, the ? kernels are constructed using the support sets S(p) and S(:p). Only the graded propositions are added to the constructed ?-kernels as non-graded propositions always survive telescoping. The fused grade of all the propositions in the constructed kernels are computed. For each kernel, the propositions with the least fused grade are removed from the set of telescoped supports of the current context, disbelieving the propositions. The contradictions handling algorithm is shown in Figure 4.
else Input: - Current supported knowledge base KB = hP; S; Gi - Contradictory propositions p 2 P and :p 2 P - Current context C = hHS; T Si, - Grade fusion operators and . ?-kernels = ? if Either p or :p is graded then if p is graded then
For each derived s = fO; T g 2 S(:p) f ?-kernels = ?-kernels [ ffT [ fpggg g For each derived s = fO; T g 2 S(p) ?-kernels = ?-kernels [ ffT [ f:pggg g f end end For each s1 = fO1; T1g 2 S(p) and s2 = fO2; T2g 2 S(:p) f ?-kernels = ?-kernels [ ffT1 [ T2gg g ComputeGrades(? kernels; ; ) //computes the fused grades of each proposition in each kernel in ?-kernels. For each kernel k in ?-kernels do f min = MinimumGrade(k) // gets the propositions with the minimum fused grade in k T S = T S min g In order to define a notion of graded derivation corresponding to the notion of graded consequence described in Definition 3.7, an order must be enforced between applying the rules of classical inference, applying the rule of telescoping, and handling contradictions. Just like graded consequence, graded derivation is defined at a nesting depth n.
Definition 5.5. A supported knowledge base KB = hP; S; Gi j n iff is asserted in the current context after performing the following three steps n times: 1. Forward chain with every proposition p 2 P on the classical rules of inference.
sitions in the resulting KB after the forward chaining.
5.5
In this section, the discussion of soundness and completeness will be restricted to the class of finite LogAG theories with the unique names assumption. The formal proofs of the the arguments presented in this section will be reserved for a longer version of this paper.
In general, the proposed proof theory using j is not sound. The main reason behind that is the uncomputability of all the ?-kernels due to the undecidability of FOL. The proof theory provides an alternative way to computing all the ?-kernels by making use of the supports of the propositions. Since not all the ?-kernels can be constructed from the set of supports, some propositions in the non-constructed kernels will remain asserted after running the contradictions handling algorithm as the algorithm removes the propositions with the least grade only from the constructed kernels. Accordingly, some propositions might be derived using j from, but are not logically implied using j' by, a LogAG theory. Such unsound inferences can block the derivation of other propositions that are logically implied at successive nesting levels. This results in the proof theory being not complete as well.
It is worth noting though that the presented proof theory will be sound and complete if and only if LogAG theories are restricted to decidable fragments of FOL such as those discussed in [Bo¨rger et al., 2001]. This can be accomplished by restricting LogAG theories to be finite where all I terms are only constants and variables, no functional terms other than G are allowed to have P terms as arguments, and no quantifiers or logical connectives except : should appear in
P terms inside G. Under these restrictions, each P term can be replaced by a propositional symbol. We can then perform inferences on the propositionalized theory from which computing the ? kernels will be decidable. 6
In this section we show running traces from an implementation we developed of the LogAG proof theory in the SNePS reasoning and acting system originally developed at University at Buffalo [Shapiro, 2000]. We refer to the graded version of SNePS as GSNePS [Ehab, 2016]. We will illustrate how the examples can be represented in GSNePS, and how the implemented LogAG proof theory in GSNePS can be used to derive conclusions from uncertain information.
You know that Nixon was both a Quaker and a Republican. It is arguable though how devout a Quacker Nixon was. You also know that usually Quackers are Pacifists, and Republicans are not Pacifists. How do you decide whether Nixon was a Pacifist given being a Quacker, or not a Pacifist given being a Republican? One way of representing the above situation in GSNePS is as shown in Figure 5.
WFF2: G(Quacker(Nixon),6).
WFF4: G(Republican(Nixon),10).
WFF9: all(x)(Quacker(x) => G(Pacifist(x), 10)). WFF13: all(x)(Republican(x) => G(˜Pacifist(x),10)). sulting in a contradiction. To resolve the contradiction, the ? kernels are first constructed using the supports of the contradicting propositions as illustrated by the contradictions handling algorithm in Figure 4. The proposition with the least grade (WFF1) is removed from the current context disbelieving WFF1 and depriving WFF7 of one of its supports. Accordingly WFF7 is disasserted and we end up believing that Nixon is not a pacifist.
It is worth noting that one other possible way of representing this example is to grade the entire rules in WFF9 and WFF13 (de-dicto representation). Accordingly, the constructed ?-kernel will include both rules instead of WFF7 and WFF11. If WFF9 for instance happens to have the least grade, we will end up disbelieving the whole rule depriving Pacifist(Nixon) of one of its supports and disasserting it. However, disasserting the whole rule will result in blocking the derivation of any other individual being a pacifist given him being a quacker. This will not be the case given the de-re representation since only the consequent is disasserted.
You open the Daily Planet and read a report by Lois Lane claiming that Superman was seen in downtown Metropolis at noon. You happen to have seen Clark Kent at his office at noon, and you have always had a feeling that Superman is Clark Kent. What should you believe about the whereabouts of Superman if you trust Lois Lane’s honesty, you only mildly trust the Daily Planet, and you still have your doubts about whether Superman is indeed Clark Kent?
One way of representing the above example in GSNePS is as shown in Figure 7. Since At(SM,DT,NOON) is obtained WFF3: G(G(At(SM,DT,NOON),11),4).
WFF4: At(KC,Office,NOON).
WFF6: G(all(l,t)(At(KC,l,t)<=>At(SM,l,t)),10.5). WFF7: all(l1,l2,x,t)((Disjoint(l1,l2) and At(x,l1,t)) => ˜At(x,l2,t)).
WFF8: Disjoint(Office,DT). from a chain of two uncertain sources (Lois Lane and the Daily Planet), it is represented as a chain of grading propositions. Since we trust Lois Lane more than the Daily Planet, we assign to At(SM,DT,NOON) a grade of 11, and the graded proposition G(At(SM,DT,NOON),11) a grade of 4. This illustrates one possible use for the nesting of grading propositions to indicate the varying degrees of trust of a chain of knowledge sources. We assign to our uncertain belief that Superman is Clark Kent (and hence Superman will always be in the same location as Clark Kent) a grade of 10.5.
We ask the knowledge base next if At(SM,DT,NOON). The graded proposition At(SM, DT, NOON) (WFF1) is telescoped with a grade of 7.5 ( = mean and = max) by applying the telescoping rule of inference on WFF3. Similarly, the graded rule (WFF5) in WFF6 is telescoped with a grade of 10.5. Using the graded rule and WFF4, At(SM,Office,Noon) will be derived. Given At(SM,Office,NOON) together with WFF7 and WFF8, ˜At(SM,DT,NOON) will be derived contradicting with WFF1. To resolve the contradiction, the proposition with the least grade (WFF1) is removed from the constructed ? kernel and from the current context disbelieving WFF1. : AT(SM,DT,NOON)? Contradiction derived between WFF11: ˜AT(SM,DT,NOON) <DER,{WFF4,WFF6,WFF7,WFF8},{WFF5(10.5)}>}} and WFF!: AT(SM,DT,NOON) <TEL,{WFF3},{WFF1(7.5),WFF2(4)}> The construced bottom kernels are {WFF5(10.5), WFF1(7.5)}.
From {WFF5 WFF1}, WFF1! will be removed.
The updated current context is ((HS (WFF8 WFF7 WFF6 WFF4 WFF3))(TS (WFF5 WFF2)) WFF11!: ˜AT(SM,DT,NOON) <DER,{WFF4,WFF6,WFF7,WFF8},{WFF5}> WFF1: AT(SM,DT,NOON) <TEL,{WFF3},{WFF1,WFF2}>
Note that if the degree of trust in the Daily Planet is increased to 15, the grade of WFF1 will increase to 13. In this case, WFF5 will be removed from the current context disasserting WFF11 instead. 7
In this paper, we presented LogAG, a weighted nonmonotonic logic for reasoning with uncertainty. Not withstanding the abundance of graded logics in the literature, it is our conviction that LogAG provides an interesting alternative. We hope to have demonstrated the utility of LogAG in uncertain reasoning with graded propositions based on an algebraic framework as an alternative to the commonly used modal frameworks employed by the other graded logics in the literature. The main power of LogAG is the ability to express a chain of graded propositions where the grades are amenable to reasoning and quantification which is not the case in many other graded logics. We showed in this paper the utility of LogAG in reasoning with information provided by a chain of sources of varying degrees of trust. LogAG is also demonstrably useful in other types of commonsense reasoning including default reasoning and reasoning with paradoxical sentences as discussed in [Ehab, 2016; Ismail and Ehab, 2015]. As a next step, we plan to to carefully investigate how LogAG relates to other graded logics and non-monotonic formalisms. We have some preliminary results showing that LogAG subsumes circumscription, some default theories, and Nute’s defeasible logic [Nute, 2001].
Theories of properties, re