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 Log A G for reasoning with uncertain beliefs by presenting its proof theory. The syntax and semantics of Log A G is thoroughly described in [Ehab, 2016;Ismail and Ehab, 2015]. "Log" stands for logic, "A" for algebraic, and "G" for grades. In Log A G, 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, Log A G is a logic for reasoning about graded propositions. Log A G 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 Log A G 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;Milošević and Ognjanović, 2012] may be used to express graded grading propositions too, unlike Log A G, 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 Log A G. This makes Log A G 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], Log A G is a nonmodal logic with classical notions of worlds and truth values. This is not to say that Log A G 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, Log A G 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 Log A G are reviewed. In Section 4, we show that Log A G 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 Log A G proof theory discussing its soundness and completeness. Finally, we show running examples from an implementation of Log A G in Section 6 demonstrating the utility of Log A G in non-monotonic reasoning and in reasoning about information provided by a chain of sources of varying degrees of trust.
Log A G consists of algebraically constructed terms from function symbols. There are no sentences in Log A G; instead, we use terms of a distinguished syntactic type to denote propositions. Propositions are included as first-class individuals in the Log A G 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 Log A G 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 Log A G alphabet includes a non-empty, countable set of constant and function symbols each having a syntactic sort from the set σ = {σ P , σ D , σ I } ∪ {τ 1 −→ τ 2 | τ 1 ∈ {σ P , σ D , σ I }} and τ 2 ∈ σ} 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, Log A G 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 ∀; and a set of logical symbols defined as the union of the following sets:
We will begin this section by presenting the interpretation of the Log A G 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.
A key element of defining the semantics of Log A G is the notion of a Log A G structure. Definition 3.1. A Log A G structure is a quintuple S = D, A, g, <, e , 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.
is a complete, non-degenerate Boolean algebra.
• g : P × G −→ P is a grading function.
• <: G × G −→ P is an ordering function.
• e : G × G −→ {⊥, } is an equality function, where for every g 1 , g 2 ∈ G: e(g 1 , g 2 ) = if g 1 = g 2 , and e(g 1 , g 2 ) = ⊥ 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 ∈ P and a grade g ∈ G to the proposition that the grade of p is g. By not imposing any further restrictions on g, we allow any reasonable notion of grading. < is an ordering function on the grades in G. It maps two grades g 1 and g 2 to the proposition that g 1 is less than g 2 . 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 Log A G language is a triple S, V f , V x , where S is a Log A G structure, V f is a function that assigns to each function symbol an appropriate function on D, and V x is a function mapping each variable to a corresponding element of the appropriate block of D. An interpretation of Log A G terms is given by a function [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 Log A G language. For every φ ∈ σ P and Γ ⊆ σ P , φ is a logical consequence of Γ, denoted
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, F1 (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 {p, p ⇒ q} and {p, p ⇒ r} 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 F2 (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 d 1 , and ¬q is graded in a grading chain containing d 1 and d 2 . To get a fused grade for ¬q, we will combine both d 1 and d 2 . If d 1 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 F3 (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 Log A G, 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 ⊕. Definition 3.3. Let S be a Log A G structure with a depthand fan-out-bounded P 2 . A telescoping structure for S is a quadruple T = T , O, ⊗, ⊕ , where
• T ⊆ P, referred to as the top theory;
• O is an ultrafilter of the subalgebra induced by Range(<) [Sankappanavar and Burris, 1981];
Recasting the familiar notion of a kernel of a belief base [Hansson, 1994]
where E(F (X )) is the set of embedded graded propositions in the filter of X . Let Q ⊥ be the set of Q kernels that entail ⊥. A proposition p ∈ 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 f T (p, Q). Definition 3.4. For a telescoping structure T = T , O, ⊗, ⊕ and a fan-in-bounded
there is some ungraded q ∈ X such that q / ∈ F (T ); or 3. there is some graded q ∈ X such that q / ∈ F (T ) and
given T}. The notion of a proposition p being supported in Q is defined as follows. Definition 3.5. Let Q, T ⊆ P. We say that p is supported in
there is a grading chain q 0 , q 1 , . . . , q n of p in Q with
Proof. If F (ς(κ(Q, T), T )) is not proper, then ς(κ(Q, T), T ) has at least one kernel X ∈ 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 E 1 (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 E 1 (F (Q)). Definition 3.6. Let T be a telescoping structure for S,
finitely-many grading propositions, then τ T (Q) is defined, for every telescoping structure T. Hence, provided that the right-hand side is defined, let
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. 4Example 3.1 in Figure 3 illustrates the construction of graded filters.
Example 3.1 Consider Q = {−p + q, −p + r, g(p, 2), g(g(−q, 2), 3)} and T = Q, O, ⊗, ⊕ where ⊕ = max, and ⊗ = mean.
. Hence, everything in E 1 (F (Q)) survives telescoping and is supported.
T ) Upon telescoping to degree 2, there are two ⊥−kernels {q, −q} and {p, −p + q, −q}. 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 / ∈ 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.
Figure 3: The construction of graded filters. We use graded filters to define graded consequence as follows. Given a Log A G theory T ⊆ σ P and a valuation Definition 3.7. Let T be a Log A G theory and V = S, V f , V x a valuation, where S has a set P which is depthand fan-out-bounded, for some Log A G language L. For every p ∈ σ P and S grading canon
does not contain any grading propositions. However, unlike |=, |
C is non-monotonic in general.
One way of evaluating non-monotonic formalisms in literature (for instance [Gabbay, 1985;Makinson, 1994]) is to examine the properties of their logical consequence relations.
Accordingly, we will briefly present in this section some properties of the Log A G consequence relation. Since according to Definition 3.7 the graded consequence relation of Log A G 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 Log A G 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 ∈ 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 ⊆ κ(E 1 (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
) is a fixed point where p ∈ F i (T 1 ), then there is some j ∈ N such that F j (T 2 ) is a fixed point and F i (T 1 ) = F j (T 2 ). Theorem 4.2. For any proposition p, let T 1 = T , O, ⊗, ⊕ and T 2 = T ∪ {p}, O, ⊗, ⊕ . Further, let F n (T 1 ) and F m (T 2 ) be fixed points where n, m ∈ N. The graded consequence relation of Log A G defined in terms of graded filters observes the following extended versions of reflexivity, cut, and cautious monotony.
1. Reflexivity: If p ∈ T , then p ∈ F n (T 1 ).
2. Cut: If p ∈ F n (T 1 ) and q ∈ F m (T 2 ), then q ∈ F n (T 1 ). 3. Cautious Monotony: If p ∈ F n (T 1 ) and q ∈ F n (T 1 ), then q ∈ F m (T 2 ).
Proof. Reflexivity follows directly from Clause 1 in Definition 3.5 and the definition of graded filters. If q ∈ F m (T 2 ), then according to Lemma 4.1 it must be the case that q ∈ F n (T 1 ). Accordingly, the graded consequence of Log A G relation observes cut.
Similarly, if p ∈ F n (T 1 ) and q ∈ F n (T 1 ), then it follow from Lemma 4.1 that q ∈ F m (T 2 ). Accordingly, the graded consequence relation of Log A G observes cautious monotony.
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 [Bö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 = HS, T S 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 = O, T where O ∪ T |= 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: Definition 5.2. A Knowledge base (KB) is defined as a triple P, S, G where:
• P ⊆ σ P .
• S is a function mapping each propositional term p ∈ P to a set of supports of p. • G is a function mapping each propositional term p ∈ P to a set of sequences of grade terms of the syntactic sort σ D . 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 = ⊗, ⊕, n the fused grade of a proposition p ∈ P is defined as follows. Definition 5.3. Let KB = P, S, G , for any proposition p ∈ P, the fused grade of p is defined as
) for every G i ∈ G(p) such that i ) ≤ n. At any point of time, not all propositional terms p ∈ P will be believed in a context. Definition 5.4. Let KB = P, S, G be a supported knowledge base. A propositional term p ∈ P is said to be asserted (believed) in a context C = HS, T S if there is a support O, T ∈ 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 ∀) 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 = P, S, G ) = KB = P , S , G ). We can think of any classical inference rule as one of the following two types5 :
1. Rules that require a particular set of premises to be in the set of propositions belonging to the KB ({p 1 , p 2 , ..., p n } ⊆ P) to derive a proposition p. The updated knowledge base KB = P , S , G where P = P ∪ {p}, S (p) = S(p) ∪ CombineSups({p 1 , p 2 , ..., p n }), and
In order to define CombineSups, two helper functions need to be defined first. The set of origin sets of a premise p is defined as
Similarly, the set of telescoped propositions supporting a proposition p is defined as 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 A support for a propositional term p, s = O, T ∈ S(p), is a hypothesis support if O = {p}. s is a telescoped support if p ∈ T . Otherwise, s is a derived support.
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.
In order to define a notion 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 = P, S, G |∼ n φ iff φ is asserted in the current context after performing the following three steps n times:
1. Forward chain with every proposition p ∈ P on the classical rules of inference. 2. Apply the rule of telescoping once to all graded propositions in the resulting KB after the forward chaining. 3. Handle the contradictions according to the contradictions handling algorithm.
In this section, the discussion of soundness and completeness will be restricted to the class of finite Log A G 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 |∼ 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 |∼ from, but are not logically implied using | by, a Log A G 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 Log A G theories are restricted to decidable fragments of FOL such as those discussed in [Börger et al., 2001]. This can be accomplished by restricting Log A G 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.
In this section we show running traces from an implementation we developed of the Log A G 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 Log A G proof theory in GSNePS can be used to derive conclusions from uncertain information.
Example 6-1: Nixon's Diamond 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. In what follows, asserted well-formed formulas will be appended with a "!". The supports of the propositions are shown with each proposition annotated with one of two support types: telescoped (TEL), or derived (DER).
We ask the knowledge base next if Nixon is a Pacifist. The result of the query is shown in Figure 6. First, the telescoping rule of inference is applied on WFF2 deriving Quacker(Nixon)(WFF1). Similarly, Republican(Nixon)(WFF3) is telescoped from WFF4. Both WFF1 and the rule WFF9 are used to derive G(Pacifist(Nixon),10)(WFF8). Similarly, WFF3 and the rule WFF13 are used to derive G(˜Pacifist(Nixon),10)(WFF12) at nesting depth level 1. At the next nesting depth level, the telescoping rule of inference is applied on both WFF8 and WFF12 to derive Pacifist(Nixon) and ˜Pacifist(Nixon) re-: Pacifist(Nixon)? Contradiction derived between WFF7: PACIFIST(NIXON) <TEL,{WFF2,WFF9},{WFF1,WFF7}> and WFF11: ˜PACIFIST(NIXON) <TEL,{WFF3,WFF13},{WFF3,WFF11}>
The construced bottom kernels are {WFF1(6), WFF3(10), WFF7(10), WFF11(10)}. From {WFF1, WFF3, WFF7,WFF11}, WFF1! will be removed. The updated current context is ((HS (WFF13 WFF9 WFF4 WFF2)) (TS (WFF11 WFF7 WFF3))) WFF7: PACIFIST(NIXON) <TEL,{WFF2,WFF7},{WFF1,WFF10}> WFF11!: ˜PACIFIST(NIXON) <TEL,WFF5,WFF13,WFF4,WFF16> 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.
Example 6-2: The Case of Superman 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 Figure 7: The Case of Superman in GSNePS 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 Su-perman 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. 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.
In this paper, we presented Log A G, a weighted nonmonotonic logic for reasoning with uncertainty. Not withstanding the abundance of graded logics in the literature, it is our conviction that Log A G provides an interesting alternative. We hope to have demonstrated the utility of Log A G 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 Log A G 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 Log A G in reasoning with information provided by a chain of sources of varying degrees of trust. Log A G 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 Log A G relates to other graded logics and non-monotonic formalisms. We have some preliminary results showing that Log A G subsumes circumscription, some default theories, and Nute's defeasible logic [Nute, 2001].