=Paper=
{{Paper
|id=Vol-2052/paper8
|storemode=property
|title=LogAG: An Algebraic Non-Monotonic Logic for Reasoning with Uncertainty
|pdfUrl=https://ceur-ws.org/Vol-2052/paper8.pdf
|volume=Vol-2052
|authors=Nourhan Ehab,Haythem Ismail
|dblpUrl=https://dblp.org/rec/conf/commonsense/EhabI17
}}
==LogAG: An Algebraic Non-Monotonic Logic for Reasoning with Uncertainty==
https://ceur-ws.org/Vol-2052/paper8.pdf
LogA G: An Algebraic Non-Monotonic Logic for Reasoning with Uncertainty
Nourhan Ehab Haythem O. Ismail
German University in Cairo Cairo University
Egypt German University in Cairo
Egypt
Abstract some multimodal logics such as [Demolombe and Liau, 2001;
Milošević and Ognjanović, 2012] may be used to express
We present a weighted algebraic non-monotonic
graded grading propositions too, unlike LogA G, the grades
logic we refer to as LogA G for reasoning with
themselves are embedded in the modal operators and are
uncertain beliefs. In LogA G, the classical logical
not amenable to reasoning and quantification. We will show
formulas could be associated with ordered grades
throughout this paper that this is not the case with LogA G.
representing measures of uncertainty. The revision
This makes LogA G a quite expressive language that is still
of beliefs in LogA G, when contradictions arise,
intuitive and very similar in syntax to first-order logic.
is done according to the grades of the contradic-
tory propositions. Throughout the paper, we present While most of the weighted logics we are aware of em-
the syntax and semantics of LogA G, extending the ploy non-classical modal logic semantics by assigning grades
classical notion of logical consequence to handle to possible worlds [Dubois et al., 2014], LogA G is a non-
graded propositions. A proof theory for LogA G is modal logic with classical notions of worlds and truth val-
thoroughly described, discussing its soundness and ues. This is not to say that LogA G is a classical logic, but it
completeness. Finally, we demonstrate the utility is closer in spirit to classical non-monotonic logics such as
of LogA G in non-monotonic reasoning and in rea- default logic [Reiter, 1980] and circumscription [McCarthy,
soning about information provided by a chain of 1980]. Following these formalisms, LogA G assumes a clas-
sources of varying degrees of trust. sical 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
1 Introduction take the algebraic, rather than the modal, route.
Most of the commonsense reasoning we perform in our every- In Sections 2 and 3, the syntax and semantics of LogA G
day lives typically involves uncertain, possibly contradicting, are reviewed. In Section 4, we show that LogA G is a stable
beliefs. Consequently, any intelligent agent emulating human and well-behaved non-monotonic logic by discussing some
reasoning must be able to handle uncertain knowledge in a of the properties of the extended logical consequence rela-
way that facilitates drawing reasonable conclusions, and re- tion. Next, we present in Section 5 the LogA G proof theory
solve contradictions when they arise. Tremendous research discussing its soundness and completeness. Finally, we show
effort has been made over the years to attempt to understand running examples from an implementation of LogA G in Sec-
and model uncertain reasoning [Halpern, 2017]. The work tion 6 demonstrating the utility of LogA G in non-monotonic
presented in this paper is one such attempt. reasoning and in reasoning about information provided by a
In this paper, we extend a logic we refer to as LogA G chain of sources of varying degrees of trust.
for reasoning with uncertain beliefs by presenting its proof
theory. The syntax and semantics of LogA G is thoroughly 2 LogA G Syntax
described in [Ehab, 2016; Ismail and Ehab, 2015]. “Log”
stands for logic, “A” for algebraic, and “G” for grades. In LogA G consists of algebraically constructed terms from
LogA G, a classical logical formula could be associated with function symbols. There are no sentences in LogA G; in-
a grade representing a measure of its uncertainty. Non-graded stead, we use terms of a distinguished syntactic type to denote
formulas are taken to be certain. In this way, LogA G is a propositions. Propositions are included as first-class individ-
logic for reasoning about graded propositions. LogA G is al- uals in the LogA G ontology and are structured in a Boolean
gebraic in that it is a language of only terms, some of which algebra giving us all standard truth conditions and classi-
denote propositions. Both propositions and their grades are cal notions of consequence and validity. The inclusion of
taken as individuals in the LogA G ontology. Thus, the lan- propositions in the ontology, though non-standard, has been
guage includes terms denoting graded propositions, grades suggested by several authors [Church, 1950; Bealer, 1979;
of propositions, grading propositions, and graded grading Parsons, 1993; Shapiro, 1993]. Additionally, grades are in-
propositions in an arbitrary compositional structure. While troduced as first-class individuals in the ontology. As a result,
propositions about graded propositions can be constructed,
which are themselves recursively gradable.
A LogA 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 denot-
ing grades, and σI is a set of terms denoting anything else. A
LogA G alphabet includes a non-empty, countable set of con-
stant 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 Figure 1: The interpretation of the LogA G terms.
of sort σP , σD , or σI and produce a functional term of sort τ2 .
(Given the restriction of the first argument of function sym- notion of grading. < is an ordering function on the grades in
bols to base sorts, LogA G is, in a sense, a first-order lan- G. It maps two grades g1 and g2 to the proposition that g1
guage.) In addition, an alphabet includes a countably infinite is less than g2 . Some restrictions are imposed on < as men-
set of variables of the three base sorts; a set of syncategore- tioned in [Ismail and Ehab, 2015] to give rise to an irreflexive
matic symbols including the comma, various matching pairs linear order on G which is serial in both directions.
of brackets and parentheses, and the symbol ∀; and a set of A valuation V of a LogA G language is a triple
logical symbols defined as the union of the following sets: hS, Vf , Vx i, where S is a LogA G structure, Vf is a function
.
{¬} ⊆ σP −→ σP , {∧, ∨} ⊆ σP −→ σP −→ σP , {≺, = that assigns to each function symbol an appropriate function
} ⊆ σD −→ σD −→ σP , and {G} ⊆ σP −→ σD −→ σP . 1 on D, and Vx is a function mapping each variable to a cor-
responding element of the appropriate block of D. An inter-
3 LogA G Semantics pretation of LogA G terms is given by a function [[·]]V . Figure
1 summarizes the operation of [[·]]V . The formal definition of
We will begin this section by presenting the interpretation of
[[·]]V can be found in [Ismail and Ehab, 2015].
the LogA G syntactic structures along with the algebraic def-
inition of logical consequence. Next, we will thoroughly de- We define logical consequence using the familiar notion
scribe our proposed extension of logical consequence to ad- of filters from Boolean algebra [Sankappanavar and Burris,
dress uncertain reasoning with graded propositions. Through- 1981]. A propositional term φ is a logical consequence of a
out this section, only sketches of the proofs will be shown for set of propositional terms Γ if it is a member of the filter of
space limitations. the interpretation of Γ, denoted F ([[Γ]]V ).
Definition 3.2. Let L be a LogA G language. For every φ ∈
3.1 Logical Consequence σP and Γ ⊆ σP , φ is a logical consequence of Γ, denoted
V V
A key element of defining the semantics of LogA G is the Γ |= φ, if,
Yfor every L-valuation V, [[φ]] ∈ F ([[Γ]] ) where
notion of a LogA G structure. V V
[[Γ]] = [[γ]] .
Definition 3.1. A LogA G structure is a quintuple γ∈Γ
S = hD, A, g, <, ei, where
3.2 Graded Consequence
• D, the domain of discourse, is a set with two dis-
joint, non-empty, countable subsets: P denoting a set The definition of logical consequence presented in the previ-
of propositional terms, and G denoting a set of grading ous section cannot address uncertain reasoning with graded
terms. propositions. To see that, consider an agent reasoning with a
• A = hP, +, ·, −, ⊥, >i is a complete, non-degenerate set of propositional terms Q as shown in Figure 2. It would
Boolean algebra. make sense for the agent to be able to conclude p even if
p is uncertain (and, hence, graded) since it has no reason
• g : P × G −→ P is a grading function. to believe ¬p. The filter F (Q), however, contains the clas-
• <: G × G −→ P is an ordering function. sical logical consequences of Q, but will never contain p. For
• e : G × G −→ {⊥, >} is an equality function, where for this reason, we extend our classical notion of filters into a
every g1 , g2 ∈ G: more liberal notion of graded filters to enable the agent to
e(g1 , g2 ) = > if g1 = g2 , and e(g1 , g2 ) = ⊥ otherwise. conclude, in addition to the classical logical consequences of
The three blocks of the domain of discourse P, G, and Q, propositions that are graded in Q or follow from graded
P ∪ G stand in correspondence to the three base syntactic propositions in Q. This should be done without introducing
sorts σP , σD , and σI respectively. The set of propositions P inconsistencies. Due to nested grading, graded filters come
is interpreted by a complete, non-degenerate Boolean algebra in degrees depending on the depth of nesting of the admitted
A. g is a function that maps a proposition p ∈ P and a grade graded propositions. In Figure 2, F 1 (Q) is the graded filter
g ∈ G to the proposition that the grade of p is g. By not im- of degree 1. F 1 (Q) contains everything in F (Q) in addition
posing any further restrictions on g, we allow any reasonable 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 classi-
1
Terms involving ⇒, ⇔, and ∃ can always be expressed in terms cally from {p, p ⇒ q} and {p, p ⇒ r} respectively. To com-
of the above logical operators and ∀. pute the graded filter of degree 2, F 2 (Q), we take everything
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 weak-
est 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).
Definition 3.4. For a telescoping structure T =
hT , O, ⊗, ⊕i and a fan-in-bounded 3 Q ⊆ P, if X ⊆ Q,
then p ∈ X survives X given T if
1. p is ungraded in Q; or
2. there is some ungraded q ∈ X such that q ∈ / F (T ); or
Figure 2: Graded Filters
3. there is some graded q ∈ X such that q ∈ / F (T ) and
1
in F (Q) and try to add the graded proposition ¬q at depth (fT (q, Q) < fT (p, Q)) ∈ O.
2. The problem is, once we do that, we have a contradiction The set of kernel survivors of Q given T is the set
with q. To resolve the contradiction, we admit to F 2 (Q) ei-
ther p (and consequently q and r) or ¬q. In deciding which of κ(Q, T) = {p ∈ Q| if p ∈ X ∈ Q ⊥ then p survives X
p and ¬q to kick out we will allude to their grades. The grade given T}.
of p is d1 , and ¬q is graded in a grading chain containing d1 The notion of a proposition p being supported in Q is de-
and d2 . To get a fused grade for ¬q, we will combine both d1 fined as follows.
and d2 . If d1 is less than the fused grade of ¬q, p will not be Definition 3.5. Let Q, T ⊆ P. We say that p is supported in
admitted to the graded filter, together with its consequences Q given T if
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 1. p ∈ F (T ); or
in F 2 (Q) reaching a fixed point. In general, the elements of 2. there is a grading chain hq0 , q1 , . . . , qn i of p in Q with
F i (Q) will be referred to as the graded consequences at depth q0 ∈ F (R) where every member of R is supported in Q.
i. In what follows, graded filters will be formally defined. The set of propositions supported in Q given T is denoted by
The key to defining graded filters is the intuition that the ς(Q, T ).
set of consequences of a proposition set Q may be further Observation 1. If F (T ) is proper, then F (ς(κ(Q, T), T )) is
enriched by telescoping Q and accepting some of the propo- proper.
sitions graded therein. For this, we need to define (i) the pro-
cess of telescoping, which is a step-wise process that consid- Proof. If F (ς(κ(Q, T), T )) is not proper, then ς(κ(Q, T), T )
ers propositions at increasing grading depths, and (ii) a cri- has at least one kernel X ∈ Q ⊥. According to Definitions
terion for accepting graded propositions which, as mentioned 3.4 and 3.5, this can only happen if X ⊆ T . Thus, F (T ) is
before, depends on the grades of said propositions. Since the proper.
nesting of grading chains is permissible in LogA G, it is nec-
essary to compute the fused grade of a graded proposition p In what follows, the graded propositions at depth 1 of the
in a chain C to decide whether it will be accepted or not. The filter of Q will be denoted as E 1 (F (Q)). The T-induced tele-
fusion of grades in a chain is done according to an opera- scoping of Q is defined as the set of propositions supported
tor ⊗. Further, since a graded proposition p might be graded given T in the set of kernel survivors of E 1 (F (Q)).
by more than one grading chain, we define the notion of the Definition 3.6. Let T be a telescoping structure for S, If Q ⊂
fused grade of p across all the chains grading it by an operator P such that E 1 (F (Q)) is fan-in-bounded, then the T-induced
⊕. telescoping of Q is given by
Definition 3.3. Let S be a LogA G structure with a depth- τT (Q) = ς(κ(E 1 (F (Q)), T), T ).
and fan-out-bounded P 2 . A telescoping structure for S is a If F (Q) has finitely-many grading propositions, then
quadruple T = hT , O, ⊗, ⊕i, where τT (Q) is defined, for every telescoping structure T. Hence,
• T ⊆ P, referred to as the top theory; provided that the right-hand side is defined, let
• O is an ultrafilter of the subalgebra induced by
Q if n = 0
Range(<) [Sankappanavar and Burris, 1981]; τTn (Q) =
S∞ S∞ τT (τTn−1 (Q)) otherwise
• ⊗ : i=1 G i −→ G; and ⊕ : i=1 G i −→ G. Finally, a graded filter of a top theory T , denoted F n (T),
Recasting the familiar notion of a kernel of a belief base is defined as the filter of the T-induced telescoping of T of
[Hansson, 1994] into the context of LogA G structures, we degree n.4
say that a ⊥-kernel of Q ⊆ P is a subset-minimal inconsis- 3
tent set X ⊆ Q such that F (E(F (X ))) is improper (= P) Q is fan-in-bounded if every graded proposition is graded by at
most fin grading propositions.
2 4
P is depth-bounded if every grading chain has at most d distinct In general, even with a finite and fan-in-bounded T , the exis-
grading propositions and is fan-out-bounded if every grading propo- tence of a fixed-point for graded filters is not secured as discussed in
sition grades at most fout propositions [Ismail and Ehab, 2015]. [Ismail and Ehab, 2015].
Example 3.1 in Figure 3 illustrates the construction of graded filters of a consistent theory are always consistent.
graded filters. This implies that reasoning in LogA G is consistency preserv-
ing.
Example 3.1 Theorem 4.1. If T is a telescoping structure where F (T ) is
Consider Q = {−p + q, −p + r, g(p, 2), g(g(−q, 2), 3)} and T =
hQ, O, ⊗, ⊕i where ⊕ = max, and ⊗ = mean.
proper, then, if defined, F n (T) is proper, for every n ∈ N.
0
• τT =Q Proof. For n = 0, the statement is trivial, since F 0 (T) =
• 1
τT 0
= τT (τT ) = ς(κ(E 1 (F (Q)), T), T ) F (T ). Otherwise, the statement follows directly from Obser-
F (Q) = Q ∪ {−p + q.g(p, 2), g(g(−q, 2), 3) + g(p, 2), ....} vation 1 since, by the definition of graded filters, F k+1 (T) =
E 1 (F (Q) = F (Q) ∪ {p, g(−q, 2)}
κ(E 1 (F (Q), T) = E 1 (F (Q) F (K), for some K ⊆ κ(E 1 (F k (T)), T).
1
τT = κ(E 1 (F (Q), T) = ς(κ(E 1 (F (Q), T), Q)
F 1 (T) = F (τT 1
) A widely accepted view of Gabbay [Gabbay, 1985] for as-
Upon telescoping to degree 1, there are no contradictions in E 1 (F (Q)) sessing whether a formalism is considered to be a reasonable
(no X ⊆ E (F (Q)). Hence, everything in E 1 (F (Q)) survives tele-
1
non-monotonic logic asserts that reasoning the formalism’s
scoping and is supported.
2 1
logical consequence relation should observe reflexivity, cut,
• τT = τT (τT )
1 1
E (F (τT )) = F (τT 1
) ∪ {−q}
and cautious monotony.
κ(E 1 (F (τT 1
)), T) = F (τT 1
) − {p} The following lemma will be useful in the proof of the fol-
τT = ς(κ(E (F (τT )), T), Q) = κ(E 1 (F (τT
2 1 1 1
)), T) − {q, r} lowing theorem.
F 2 (T) = F (τT 2
)
Upon telescoping to degree 2, there are two ⊥−kernels {q, −q} and Lemma 4.1. For any proposition p, let T1 = hT , O, ⊗, ⊕i,
{p, −p + q, −q}. q survives the first kernel as it is not graded in Q. T2 = hT ∪ {p}, O, ⊗, ⊕i, and i ∈ N. If F i (T1 ) is a fixed
−q survives the first kernel as well as it is the only graded proposition in point where p ∈ F i (T1 ), then there is some j ∈ N such that
the kernel with another member q ∈ / F (Q). p does not survive the sec-
ond kernel as the kernel contains another graded proposition −q and the F j (T2 ) is a fixed point and F i (T1 ) = F j (T2 ).
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. Theorem 4.2. For any proposition p, let T1 = hT , O, ⊗, ⊕i
The graded filter of degree 2 does not contain p, q or r. and T2 = hT ∪ {p}, O, ⊗, ⊕i. Further, let F n (T1 ) and
3
• τT 2
= τT (τT ) F m (T2 ) be fixed points where n, m ∈ N. The graded conse-
3
τT = ς(κ(E 1 (F (τT2
)), T), Q) = κ(E 1 (F (τT 2
)), T) quence relation of LogA G defined in terms of graded filters
F 3 (T) = F (τT3
) = F 2 (T) reaching a fixed point. observes the following extended versions of reflexivity, cut,
and cautious monotony.
Figure 3: The construction of graded filters.
We use graded filters to define graded consequence as 1. Reflexivity: If p ∈ T , then p ∈ F n (T1 ).
follows. Given a LogA G theory T ⊆ σP and a valuation 2. Cut: If p ∈ F n (T1 ) and q ∈ F m (T2 ),
V = hS, Vf , Vx i, let V(T) = {[[p]]V | p ∈ T}. Further, then q ∈ F n (T1 ).
for a LogA G structure S, an S grading canon is a triple 3. Cautious Monotony: If p ∈ F n (T1 ) and q ∈ F n (T1 ),
C = h⊗, ⊕, ni where n ∈ N and ⊗ and ⊕ are as indicated then q ∈ F m (T2 ).
in Definition 3.3.
Proof. Reflexivity follows directly from Clause 1 in Defini-
Definition 3.7. Let T be a LogA G theory and V = tion 3.5 and the definition of graded filters.
hS, Vf , Vx i a valuation, where S has a set P which is depth- If q ∈ F m (T2 ), then according to Lemma 4.1 it must be
and fan-out-bounded, for some LogA G language L. For ev- the case that q ∈ F n (T1 ). Accordingly, the graded conse-
ery p ∈ σP and S grading canon C = h⊗, ⊕, ni, p is a quence of LogA G relation observes cut.
C
graded consequence of T with respect to C, denoted T |' p, Similarly, if p ∈ F n (T1 ) and q ∈ F n (T1 ), then it follow
n V n
if F (T) is defined and [[p]] ∈ F (T), for every telescop- from Lemma 4.1 that q ∈ F m (T2 ). Accordingly, the graded
ing structure T = hV(T), O, ⊗, ⊕i for S, where O extends consequence relation of LogA G observes cautious monotony.
F (V(T) ∩ Range(<)). (An ultrafilter U extends a filter F , if
F ⊆ U .)
C
It is worth noting that |' reduces to |= if n = 0 or 5 LogA G Proof Theory
if F (E(V(T))) does not contain any grading propositions. In order to compute the graded filter of degree n, all ⊥-
C kernels are to be computed, which is undecidable for first-
However, unlike |=, |' is non-monotonic in general.
order logic according to Church’s Theorem [Börger et al.,
2001; Raatikainen, 2015]. For this reason, the proposed proof
4 Properties of LogA G theory takes an alternative approach. A set of supports is kept
One way of evaluating non-monotonic formalisms in litera- track of for every proposition enabling the computation of
ture (for instance [Gabbay, 1985; Makinson, 1994]) is to ex- some of the ⊥-kernels. Further, the natural deduction rules of
amine the properties of their logical consequence relations. classical logic are modified to update the supports of the in-
Accordingly, we will briefly present in this section some ferred propositions, and a special derivation rule of telescop-
properties of the LogA G consequence relation. ing is added. This special rule of inference will extract any
Since according to Definition 3.7 the graded consequence graded proposition in any grading chain. It is worth noting
relation of LogA G is based on graded filters, we first present that this is different from our semantic notion of telescop-
a property of graded filters. The following theorem states that ing presented in the last section. As will be shown, this new
derivation rule can introduce contradictions. Hence, a way of 1. Rules that require a particular set of premises to
handling said contradictions is proposed. be in the set of propositions belonging to the KB
({p1 , p2 , ..., pn } ⊆ P) to derive a proposition p. The up-
5.1 Supported Knowledge Bases dated knowledge base KB 0 = hP0 , S0 , G0 i where P0 =
We refer to a belief space as a context. To accommodate rea- P ∪ {p}, S0 (p) = S(p) ∪ CombineSups({p1 , p2 , ..., pn }),
soning with graded propositions, a context is defined as a pair and G0 (p) = G(p) ∪ {hi}.
C = hHS, T Si where HS is a set of hypotheses (facts), and In order to define CombineSups, two helper functions
T S is a set of telescoped (graded) propositions. The context need to be defined first. The set of origin sets of a
where the current inference is done is referred to as the cur- premise p is defined as O(p) = {o | ho, ti ∈ S(p)}.
rent context. Similarly, the set of telescoped propositions supporting a
Each propositional term p is associated with a set of sup- proposition p is defined as T (p) = {t | ho, ti ∈ S(p)}.
ports, where each support corresponds to a unique derivation CombineSups({p 1 , p2 , ..., pn }) = {hO, T i | O =
of p. We extend the structure of a support suggested in [Mar- Sn
{o | o = i=1Soi where (o1 , o2 , ..., on ) ∈ ×ni=1 O(pi ) and
tins and Shapiro, 1988] to include graded supports. n
T = {t | t = i=1 ti where
Definition 5.1. A support of a proposition p is a pair s = (t1 , t2 , ..., tn ) ∈ ×ni=1 T (pi )}.
hO, T i where O ∪ T |= p. O will be referred to as the origin 2. Rules that add an assumption δ to the KB generating an
set, and T will be referred to as the telescoped supports set. updated temporary KB 00 = hP00 , S00 , G00 i where P00 = P∪
To accommodate the supports of propositions, a supported {δ}, S00 (δ) = {h{δ}, {}i}, and G00 (δ) = {hi}. If ψ is
knowledge base is defined as follows: derived from KB 00 , then some proposition p will be added
Definition 5.2. A Knowledge base (KB) is defined as a triple to KB. The updated knowledge base KB 0 = hP0 , S0 , G0 i
hP, S, Gi where: where P0 = P ∪ {p}, S0 (p) = S(p) ∪ F ilterSups(S00 (p))
where F ilterSups(S00 (p)) = {hO − {δ}, T i | hO, T i ∈
• P ⊆ σP .
S00 (p)}, and G0 (p) = G(p) ∪ {hi}i.
• S is a function mapping each propositional term p ∈ P
to a set of supports of p. In addition to the classical rules of inference, the pro-
• G is a function mapping each propositional term p ∈ P posed proof theory adds a special inference rule of telescop-
to a set of sequences of grade terms of the syntactic sort ing (T el). T el will extract a graded proposition from a grad-
σD . ing proposition, and result in a new updated supported knowl-
edge base. T el will also change the T S set of the current
In what follows, we will assume that all grade terms ap- context. The T S set of the current context will contain the
pearing in P are numerals. Each sequence in G(p) contains propositional terms telescoped using the telescoping rule of
the grades associated with p in a particular chain. This will inference from grading propositional terms in HS, or deriv-
facilitate computing the fused grade of p. Given a grading able from HS using any of the inference rules. T el is defined
canon C = h⊗, ⊕, ni the fused grade of a proposition p ∈ P as follows:
is defined as follows. Telescoping (T el):
Definition 5.3. Let KB = hP, S, Gi, for any proposi- If G(p, g) ∈ P, the updated knowledge base KB 0 =
tion p ∈ P, the fused grade of p is defined as f (p) = hP0 , S0 , T0 i where P0 = P ∪ {p}, S0 (p) = S(p) ∪ T elSup(p),
length(G(p)) and G0 (p) = G(p) ∪ T elGrades(p). T elSup(p) = {hO, T ∪
L
(f⊗ (Gi )i=1 ) for every Gi ∈ G(p) such that
length(Gi ) ≤ n. {p}i | hO, T i ∈ S(p)} and T elGrade(p) = {Gi
hgi | Gi ∈ G(G(p, g)) and denotes sequence concatena-
At any point of time, not all propositional terms p ∈ P will
tion}. The new current context is C = hHS, T S ∪ {p}i.
be believed in a context.
A support for a propositional term p, s = hO, T i ∈ S(p),
Definition 5.4. Let KB = hP, S, Gi be a supported knowl- is a hypothesis support if O = {p}. s is a telescoped support
edge base. A propositional term p ∈ P is said to be asserted if p ∈ T . Otherwise, s is a derived support.
(believed) in a context C = hHS, T Si if there is a support
hO, T i ∈ S(p) where O ⊆ HS and T ⊆ T S. 5.3 Handling Contradictions
5.2 The Inference Rules In the sequel, we assume a non-contradictory KB such that
The proposed proof theory is similar in spirit to the Fitch- any contradictions are only derived by applying the rule of
style natural deduction rules. However, it does not enforce telescoping, or by applying any sequence of inference rules
specific inference rules for the classical rules of inference (the on a minimal set containing a telescoped proposition. Once
introduction and elimination rules for ¬, ⇒, ∧, ∨, and ∀) for p and ¬p are derived, the ⊥ kernels are constructed using
the sake of generality. Any inference rule I will be applied to the support sets S(p) and S(¬p). Only the graded proposi-
a supported KB, and will result in an updated supported KB tions are added to the constructed ⊥-kernels as non-graded
(I(KB = hP, S, Gi) = KB 0 = hP0 , S0 , G0 i). We can think propositions always survive telescoping. The fused grade of
of any classical inference rule as one of the following two all the propositions in the constructed kernels are computed.
types 5 : For each kernel, the propositions with the least fused grade
are removed from the set of telescoped supports of the cur-
5 rent context, disbelieving the propositions. The contradictions
An example set of classical Fitch-style inference rules is pre-
sented in [Ehab, 2016]. handling algorithm is shown in Figure 4.
Input: - Current supported knowledge base KB = hP, S, Gi It is worth noting though that the presented proof theory
- Contradictory propositions p ∈ P and ¬p ∈ P will be sound and complete if and only if LogA G theories
- Current context C = hHS, T Si, - Grade fusion operators ⊗ and ⊕.
⊥-kernels = ∅ are restricted to decidable fragments of FOL such as those
if Either p or ¬p is graded then discussed in [Börger et al., 2001]. This can be accomplished
if p is graded then
For each derived s = {O, T } ∈ S(¬p) {
by restricting LogA G theories to be finite where all σI terms
⊥-kernels = ⊥-kernels ∪ {{T ∪ {p}}} are only constants and variables, no functional terms other
} than G are allowed to have σP terms as arguments, and no
else
For each derived s = {O, T } ∈ S(p) { quantifiers or logical connectives except ¬ should appear in
⊥-kernels = ⊥-kernels ∪ {{T ∪ {¬p}}} σP terms inside G. Under these restrictions, each σP term
} can be replaced by a propositional symbol. We can then per-
end
end form inferences on the propositionalized theory from which
For each s1 = {O1 , T1 } ∈ S(p) and s2 = {O2 , T2 } ∈ S(¬p) { computing the ⊥− kernels will be decidable.
⊥-kernels = ⊥-kernels ∪ {{T1 ∪ T2 }} }
ComputeGrades(⊥ − kernels, ⊗, ⊕)
//computes the fused grades of each proposition in each kernel in ⊥-kernels. 6 Running Examples
For each kernel k in ⊥-kernels do {
min = M inimumGrade(k) In this section we show running traces from an implementa-
// gets the propositions with the minimum fused grade in k tion we developed of the LogA G proof theory in the SNePS
T S = T S − min }
reasoning and acting system originally developed at Univer-
Figure 4: Handling Contradictions Algorithm sity at Buffalo [Shapiro, 2000]. We refer to the graded version
of SNePS as GSNePS [Ehab, 2016]. We will illustrate how
5.4 Graded Derivation the examples can be represented in GSNePS, and how the
In order to define a notion of graded derivation correspond- implemented LogA G proof theory in GSNePS can be used
ing to the notion of graded consequence described in Defi- to derive conclusions from uncertain information.
nition 3.7, an order must be enforced between applying the
rules of classical inference, applying the rule of telescoping, Example 6-1: Nixon’s Diamond
and handling contradictions. Just like graded consequence, You know that Nixon was both a Quaker and a Republican.
graded derivation is defined at a nesting depth n. It is arguable though how devout a Quacker Nixon was. You
also know that usually Quackers are Pacifists, and Republi-
Definition 5.5. A supported knowledge base KB = cans are not Pacifists. How do you decide whether Nixon was
hP, S, Gi |∼n φ iff φ is asserted in the current context after a Pacifist given being a Quacker, or not a Pacifist given being
performing the following three steps n times: a Republican? One way of representing the above situation in
1. Forward chain with every proposition p ∈ P on the clas- GSNePS is as shown in Figure 5.
sical rules of inference.
WFF2: G(Quacker(Nixon),6).
2. Apply the rule of telescoping once to all graded propo- WFF4: G(Republican(Nixon),10).
sitions in the resulting KB after the forward chaining. WFF9: all(x)(Quacker(x) => G(Pacifist(x), 10)).
WFF13: all(x)(Republican(x) => G(˜Pacifist(x),10)).
3. Handle the contradictions according to the contradic-
tions handling algorithm. Figure 5: Nixon’s Diamond in GSNePS
Since we are not sure how devout a Quacker Nixon
5.5 Soundness and Completeness of LogA G was, we assign to Quacker(Nixon) a less grade than
In this section, the discussion of soundness and completeness Republican(Nixon). We express our uncertainty in the
will be restricted to the class of finite LogA G theories with pacifism of any Quacker and non-pacifism of any Republican
the unique names assumption. The formal proofs of the the ar- by grading the consequents in WFF9 and WFF13 respectively
guments presented in this section will be reserved for a longer (de-re representation).
version of this paper. In what follows, asserted well-formed formulas will be
In general, the proposed proof theory using |∼ is not sound. appended with a “!”. The supports of the propositions are
The main reason behind that is the uncomputability of all the shown with each proposition annotated with one of two sup-
⊥-kernels due to the undecidability of FOL. The proof theory port types: telescoped (TEL), or derived (DER).
provides an alternative way to computing all the ⊥-kernels We ask the knowledge base next if Nixon is a
by making use of the supports of the propositions. Since not Pacifist. The result of the query is shown in Fig-
all the ⊥-kernels can be constructed from the set of supports, ure 6. First, the telescoping rule of inference is ap-
some propositions in the non-constructed kernels will remain plied on WFF2 deriving Quacker(Nixon)(WFF1).
asserted after running the contradictions handling algorithm Similarly, Republican(Nixon)(WFF3) is telescoped
as the algorithm removes the propositions with the least grade from WFF4. Both WFF1 and the rule WFF9 are used
only from the constructed kernels. Accordingly, some propo- to derive G(Pacifist(Nixon),10)(WFF8). Simi-
sitions might be derived using |∼ from, but are not logically larly, WFF3 and the rule WFF13 are used to derive
implied using |' by, a LogA G theory. Such unsound infer- G(˜Pacifist(Nixon),10)(WFF12) at nesting depth
ences can block the derivation of other propositions that are level 1. At the next nesting depth level, the telescoping rule
logically implied at successive nesting levels. This results in of inference is applied on both WFF8 and WFF12 to de-
the proof theory being not complete as well. rive Pacifist(Nixon) and ˜Pacifist(Nixon) re-
: Pacifist(Nixon)? perman is Clark Kent (and hence Superman will always be in
Contradiction derived between the same location as Clark Kent) a grade of 10.5.
WFF7: PACIFIST(NIXON)
and We ask the knowledge base next if At(SM,DT,NOON).
WFF11: ˜PACIFIST(NIXON) The graded proposition At(SM, DT, NOON) (WFF1) is
The construced bottom kernels are telescoped with a grade of 7.5 (⊗ = mean and ⊕ =
{WFF1(6), WFF3(10), WFF7(10), WFF11(10)}. max) by applying the telescoping rule of inference on
From {WFF1, WFF3, WFF7,WFF11}, WFF1! will be removed. WFF3. Similarly, the graded rule (WFF5) in WFF6 is tele-
The updated current context is
((HS (WFF13 WFF9 WFF4 WFF2)) (TS (WFF11 WFF7 WFF3))) scoped with a grade of 10.5. Using the graded rule and
WFF4, At(SM,Office,Noon) will be derived. Given
WFF7: PACIFIST(NIXON)
WFF11!: ˜PACIFIST(NIXON)
At(SM,Office,NOON) together with WFF7 and WFF8,
˜At(SM,DT,NOON) will be derived contradicting with
Figure 6: The Result of the Query Pacifist(Nixon) in GSNePS. WFF1. To resolve the contradiction, the proposition with
the least grade (WFF1) is removed from the constructed
sulting in a contradiction. To resolve the contradiction, the ⊥−kernel and from the current context disbelieving WFF1.
⊥−kernels are first constructed using the supports of the
contradicting propositions as illustrated by the contradictions : AT(SM,DT,NOON)?
handling algorithm in Figure 4. The proposition with the least Contradiction derived between
WFF11: ˜AT(SM,DT,NOON)
grade (WFF1) is removed from the current context disbeliev- }} and
ing WFF1 and depriving WFF7 of one of its supports. Accord- WFF!: AT(SM,DT,NOON)
ingly WFF7 is disasserted and we end up believing that Nixon
is not a pacifist. The construced bottom kernels are
It is worth noting that one other possible way of repre- {WFF5(10.5), WFF1(7.5)}.
senting this example is to grade the entire rules in WFF9 From {WFF5 WFF1}, WFF1! will be removed.
The updated current context is
and WFF13 (de-dicto representation). Accordingly, the con- ((HS (WFF8 WFF7 WFF6 WFF4 WFF3))(TS (WFF5 WFF2))
structed ⊥-kernel will include both rules instead of WFF7
WFF11!: ˜AT(SM,DT,NOON)
and WFF11. If WFF9 for instance happens to have the least
grade, we will end up disbelieving the whole rule depriving WFF1: AT(SM,DT,NOON)
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 Figure 8: The Result of the Query AT(SM,DT,NOON) in GSNePS.
him being a quacker. This will not be the case given the de-re
representation since only the consequent is disasserted. Note that if the degree of trust in the Daily Planet is in-
creased to 15, the grade of WFF1 will increase to 13. In this
Example 6-2: The Case of Superman case, WFF5 will be removed from the current context disas-
You open the Daily Planet and read a report by Lois Lane serting WFF11 instead.
claiming that Superman was seen in downtown Metropolis
at noon. You happen to have seen Clark Kent at his office at 7 Conclusion
noon, and you have always had a feeling that Superman is In this paper, we presented LogA G, a weighted non-
Clark Kent. What should you believe about the whereabouts monotonic logic for reasoning with uncertainty. Not with-
of Superman if you trust Lois Lane’s honesty, you only mildly standing the abundance of graded logics in the literature, it
trust the Daily Planet, and you still have your doubts about is our conviction that LogA G provides an interesting alter-
whether Superman is indeed Clark Kent? native. We hope to have demonstrated the utility of LogA G
One way of representing the above example in GSNePS is in uncertain reasoning with graded propositions based on
as shown in Figure 7. Since At(SM,DT,NOON) is obtained an algebraic framework as an alternative to the commonly
WFF3: G(G(At(SM,DT,NOON),11),4).
used modal frameworks employed by the other graded log-
WFF4: At(KC,Office,NOON). ics in the literature. The main power of LogA G is the ability
WFF6: G(all(l,t)(At(KC,l,t)<=>At(SM,l,t)),10.5). to express a chain of graded propositions where the grades
WFF7: all(l1,l2,x,t)((Disjoint(l1,l2) and
At(x,l1,t)) => ˜At(x,l2,t)).
are amenable to reasoning and quantification which is not
WFF8: Disjoint(Office,DT). the case in many other graded logics. We showed in this
paper the utility of LogA G in reasoning with information
Figure 7: The Case of Superman in GSNePS provided by a chain of sources of varying degrees of trust.
from a chain of two uncertain sources (Lois Lane and the LogA G is also demonstrably useful in other types of com-
Daily Planet), it is represented as a chain of grading proposi- monsense reasoning including default reasoning and reason-
tions. Since we trust Lois Lane more than the Daily Planet, we ing with paradoxical sentences as discussed in [Ehab, 2016;
assign to At(SM,DT,NOON) a grade of 11, and the graded Ismail and Ehab, 2015]. As a next step, we plan to to care-
proposition G(At(SM,DT,NOON),11) a grade of 4. This fully investigate how LogA G relates to other graded logics
illustrates one possible use for the nesting of grading propo- and non-monotonic formalisms. We have some preliminary
sitions to indicate the varying degrees of trust of a chain of results showing that LogA G subsumes circumscription, some
knowledge sources. We assign to our uncertain belief that Su- default theories, and Nute’s defeasible logic [Nute, 2001].
References [Reiter, 1980] Raymond Reiter. A logic for default reason-
[Bealer, 1979] George Bealer. Theories of properties, re- ing. Artificial intelligence, 13(1):81–132, 1980.
lations, and propositions. The Journal of Philosophy, [Sankappanavar and Burris, 1981] Hanamantagouda P.
76(11):634–648, 1979. Sankappanavar and Stanley Burris. A course in universal
[Börger et al., 2001] Egon Börger, Erich Grädel, and Yuri algebra. Graduate Texts Math, 78, 1981.
Gurevich. The classical decision problem. Springer Sci- [Shapiro, 1993] Stuart C. Shapiro. Belief spaces as sets of
ence & Business Media, 2001. propositions. Journal of Experimental & Theoretical Arti-
[Church, 1950] Alonzo Church. On carnap’s analysis of ficial Intelligence, 5(2-3):225–235, 1993.
statements of assertion and belief. Analysis, 10(5):97–99, [Shapiro, 2000] Stuart C. Shapiro. SNePS: a logic for natu-
1950. ral language understanding and commonsense reasoning,
[Demolombe and Liau, 2001] Robert Demolombe and natural language processing and knowledge representa-
Churnjung Liau. A logic of graded trust and belief fusion. tion: language for knowledge and knowledge for language,
In Proceedings of the 4th Workshop on Deception, Fraud 2000.
and Trust in Agent Societies, pages 13–25, 2001.
[Dubois et al., 2014] Didier Dubois, Lluis Godo, and Henri
Prade. Weighted logics for artificial intelligence–an intro-
ductory discussion. International Journal of Approximate
Reasoning, 55(9):1819–1829, 2014.
[Ehab, 2016] Nourhan Ehab. On the Use of Graded Propo-
sitions in Uncertain Non-monotonic Reasoning: With an
Application to Plant Disease Forecast. Master’s thesis,
German University in Cairo, Egypt, 2016.
[Gabbay, 1985] D. M. Gabbay. Theoretical Foundations for
Non-Monotonic Reasoning in Expert Systems, pages 439–
457. Springer Berlin Heidelberg, Berlin, Heidelberg, 1985.
[Halpern, 2017] Joseph Y Halpern. Reasoning about uncer-
tainty. MIT press, 2017.
[Hansson, 1994] Sven Ove Hansson. Kernel contraction.
The Journal of Symbolic Logic, 59(03):845–859, 1994.
[Ismail and Ehab, 2015] Haythem O. Ismail and Nourhan
Ehab. Algebraic semantics for graded propositions. Pro-
ceedings of the KI 2015 Workshop on Formal and Cogni-
tive Reasoning, pages 29–42, 2015.
[Makinson, 1994] David Makinson. General patterns in
nonmonotonic reasoning, volume III, pages 35–110. Ox-
ford University Press, 1994.
[Martins and Shapiro, 1988] Joao P. Martins and Stuart C.
Shapiro. A model for belief revision. Artificial intelli-
gence, 35(1):25–79, 1988.
[McCarthy, 1980] John McCarthy. Circumscription–a form
of nonmonotonic reasoning. Artificial Intelligence, 13:27–
39, 1980.
[Milošević and Ognjanović, 2012] Miloš Milošević and Zo-
ran Ognjanović. A first-order conditional probability logic.
Logic Journal of IGPL, 20(1):235–253, 2012.
[Nute, 2001] Donald Nute. Defeasible logic. In Interna-
tional Conference on Applications of Prolog, pages 151–
169. Springer, 2001.
[Parsons, 1993] Terence Parsons. On denoting propositions
and facts. Philosophical Perspectives, 7:441–460, 1993.
[Raatikainen, 2015] Panu Raatikainen. Gödel’s incomplete-
ness theorems. In Edward N. Zalta, editor, The Stanford
Encyclopedia of Philosophy. Spring 2015 edition, 2015.