Strength Factors: An Uncertainty System for a Quantified Modal Logic

arXiv:1705.10726v1 [] 30 May 2017

Naveen Sundar Govindarajulu
Rensselaer Polytechnic Institute
Troy, New York
naveensundarg@gmail.com

Abstract
We present a new system S for handling uncertainty in a quantified modal logic (first-order modal
logic). The system is based on both probability theory and proof theory. The system is derived from Chisholm’s epistemology. We concretize Chisholm’s system by grounding his undefined and primitive (i.e. foundational) concept of
reasonableness in probability and proof theory. S
can be useful in systems that have to interact with
humans and provide justifications for their uncertainty. As a demonstration of the system, we apply
the system to provide a solution to the lottery paradox. Another advantage of the system is that it can
be used to provide uncertainty values for counterfactual statements. Counterfactuals are statements
that an agent knows for sure are false. Among
other cases, counterfactuals are useful when systems have to explain their actions to users (If I had
not done α, then φ would have happened). Uncertainties for counterfactuals fall out naturally from
our system.
Efficient reasoning in just simple first-order logic
is a hard problem. Resolution-based first-order reasoning systems have made significant progress over
the last several decades in building systems that
have solved non-trivial tasks (even unsolved conjectures in mathematics). We present a sketch of
a novel algorithm for reasoning that extends firstorder resolution.
Finally, while there have been many systems of uncertainty for propositional logics, first-order logics
and propositional modal logics, there has been very
little work in building systems of uncertainty for
first-order modal logics. The work described below
is in progress; and once finished will address this
lack.

1

Introduction

We introduce a new system S for talking about uncertainty of
iterated beliefs in a quantified modal logic with belief operators. The quantified modal logic we use is based on the deontic cognitive event calculus (DC EC ), which belongs to the

Selmer Bringsjord
Rensselaer Polytechnic Institute
Troy, New York
selmer.bringsjord@gmail.com

family of cognitive calculi that have been used in modeling
complex cognition. Here, we use a subset of DC EC that we
term micro cognitive calculus (µC ). Specifically, we add a
system of uncertainty derived from Chisholm’s epistemology
[Chisholm, 1987].1 The system S is a work in progress and
hence the presentation here will be abstract in nature.
One of our primary motivations is to design a system of uncertainty that is easy to use in end-user facing systems. There
have been many studies that show that laypeople have difficulty understanding raw probability values (e.g. see [Kaye
and Koehler, 1991]); and we believe that our approach borrowed from philosophy can pave the way for systems that can
present uncertain statements in a more understandable format
to lay users.

2

Prior Work

Members in the family of cognitive calculi have been used
to formalize and automate highly intensional reasoning processes.2 More recently, using DC EC we have presented an
automation of the doctrine of double effect in [Govindarajulu
and Bringsjord, 2017].3 The doctrine of double effect is an
ethical principle that has been shown to be used by both untrained laypeople and experts when faced with moral dilemmas; and it plays a central role in many legal systems.
Other tasks automated by cognitive calculi include the
false-belief task [Arkoudas and Bringsjord, 2008] and akrasia (succumbing to temptation to violate moral principles)
[Bringsjord et al., 2014].4 Each cognitive calculus is a sorted
(i.e. typed) quantified modal logic (also known as sorted firstorder modal logic). Each calculus has a well-defined syntax
and proof calculus. The proof calculus is based on natural
1 See the SEP entry on Chisholm for a quick overview
of Chisholm’s epistemology: https://plato.stanford.edu/entries/
chisholm/#EpiIEpiTerPriFou.
2 By “intensional processes”, we roughly mean processes that
take into account knowledge, beliefs, desires, intentions, etc. of
agents. This is opposed to extensional systems such as pure firstorder systems that do not take into account states of minds of other
agents. This is not be confused with “intentional” systems which
would be modeled with intensional systems. See [Zalta, 1988] for a
detailed treatment of intensionality.
3 This work will be presented at IJCAI 2017.
4 Arkoudas and Bringsjord [2008] introduced the general family
of cognitive event calculi to which DC EC belongs.

deduction [Gentzen, 1935], and includes all the introduction
and elimination rules for first-order logic, as well as inference
schemata for the modal operators and related structures.
On the uncertainty and probability front, there have been
many logics of probability, see [Demey et al., 2016] for an
overview. Since our system builds upon probabilities, our
approach could use a variety of such systems. As we noted
above, there has been very little work in uncertainty systems
for first-order modal logics. Among first-order systems, the
seminal work in [Halpern, 1990] presents a first-order logic
with modified semantics to handle probabilistic statements.
We can use such a system as the foundation for our work, and
use it to define the base probability function Pr used below.
(Note that we leave Pr unspecified for now.)

3

The figure below shows the inference schemata for

DC EC . RP captures that perceptions get turned into beliefs. RB is an inference schema that lets us model idealized
agents that have their beliefs closed under the µC proof theory. While normal humans are not deductively closed, this
lets us model more closely how deliberate agents such as organizations and more strategic actors reason. Assume that
there is a background set of axioms Γ we are working with.
Inference Schemata
P(a,t1 , φ1 ), Γ ` t1 < t2
[RP ]
B(a,t2 , φ)

The Formal System

The formal system µC is a modal extension of the the event
calculus. The event calculus is a multi-sorted first-order logic
with a family of axiom sets. The exact axiom set is not important. The primary sorts in the system are shown below.
Sort

Description

Agent
Moment or Time

Human and non-human actors.
Time points and intervals. E.g. simple, such as ti , or complex, such as birthday(son( jack)).
Used for events in the domain.
Action types are abstract actions. They are instantiated at
particular times by actors. E.g.: “eating” vs. “jack eats.”
A subtype of Event for events that occur as actions by agents.
Used for representing states of the world in the event calculus.

Event
ActionType
Action
Fluent

Full DC EC has a suite of modal operators and inference
schemata. Here we focus on just two: an operator for belief B
and an operator for perception P. The syntax of and inference
schemata of the system are shown below. S is the set of all
sorts, f are the core function symbols, t shows the set of terms,
and φ is the syntax for the formulae.
Syntax

B(a,t1 , φ1 ), . . . , B(a,tm , φm ), {φ1 , . . . , φm } ` φ, Γ ` ti < t
[RB ]
B(a,t, φ)

4

The Uncertainty System S

In the uncertainty system, we augment the belief modal operators with a discrete set of uncertainty factors termed as
strength factors. The factors are not arbitrary and are based
on how derivable a proposition is for a given agent.
Chisholm’s epistemology has a primitive undefined binary
relation that he terms reasonableness with which he defines a
scale of strengths for beliefs one might have in a proposition.
Note that Chisholm’s system is agent free while ours is agentbased. Let φ ta ψ denote that φ is more reasonable than ψ
to an agent a at time t. For convenience, we define a new
operator, the withholding operator W, defined below:
W(a,t, φ) ≡ ¬B(a,t, φ) ∧ ¬B(a,t, ¬φ)

We now reproduce Chisholm’s system below. Note the formula used in the definitions below are meta-formula and not
strictly in µC .
Strength Factor Definitions

(
S ::=

Object Agent Self @ Agent ActionType Action v Event
Moment Formula Fluent Numeric



 action : Agent × ActionType → Action



initially : Fluent → Formula





holds : Fluent × Moment → Formula




 happens : Event × Moment → Formula
f ::=
 clipped : Moment × Fluent × Moment → Formula





 initiates : Event × Fluent × Moment → Formula




terminates : Event × Fluent × Moment → Formula




prior : Moment × Moment → Formula
t ::= x : S c : S f (t1 , . . . ,tn )
(
t :Formula ¬φ φ ∧ ψ φ ∨ ψ
φ ::=
P(a,t, φ) B(a,t, φ)

The above calculus lets us formalize statements of the form
“John believes now that Mary perceived that it was raining
yesterday.” One formalization could be:


∃t < now : B john, now, P mary,t, holds(raining,t)

Acceptable An agent a at time t finds φ acceptable iff withholding φ is not more reasonable than believing in φ.

 W(a,t, φ) 6ta B(a,t, φ); or
1

B (a,t, φ) ⇔ 
 ¬B(a,t, φ) ∧ ¬B(a,t, ¬φ) 6ta B(a,t, φ)
Some Presumption in Favor An agent a at time t has some
presumption in favor of φ iff believing φ at t is more reasonable than believing ¬φ at time t:


B2 (a,t, φ) ⇔ B(a,t, φ) ta B(a,t, ¬φ)
Beyond Reasonable Doubt An agent a at time t has beyond
reasonable doubt in φ iff believing φ at t is more reasonable than withholding φ at time t:


 B(a,t, φ) ta W(a,t, φ); or


B3 (a,t, φ) ⇔ 
 B(a,t, φ) ta ¬B(a,t, φ) ∧ ¬B(a,t, ¬φ)
Evident A formula φ is evident to an agent a at time t iff φ is
beyond reasonable doubt and if there is a ψ such that believing ψ is more reasonable for a at time t than believing
φ, then a is certain about ψ at time t.


B3 (a,t, φ)∧


"
#
B(a,t, ψ) ta B(a,t, φ)
B4 (a,t, φ) ⇔


 ∃ψ :
⇒B5 (a,t, ψ)
Certain An agent a at time t is certain about φ iff φ is beyond
reasonable doubt and there is no ψ such that believing ψ
is more reasonable for a at time t than believing φ.
(
B3 (a,t, φ)∧
5
B (a,t, φ) ⇔
¬∃ψ : B(a,t, ψ) ta B(a,t, φ)

The above definitions are from Chisholm but more rigorously formalized in µC . The definitions almost give us S except for the fact that ta is undefined. While Chisholm gives a
careful and informal analysis of the relation, he does not provide a more precise definition. Such a definition is needed for
automation. We provide a three clause defintion that is based
on both probabilities and proof theory.
There are many probability logics that allow us to define
probabilities over formulae. They are well studied and understood for propositional and first-order logics. Let L be the
set of all formulae in µC . Let L p be a pure first-order subset
of L . Assume that we have the following partial probability
function defined over L p 5 :
Pr : Agent × Moment × Formula 7→ R

Then we have the first clause of our definition for ta .
Clause I. Defining 
If Pr(a,t, φ) and Pr(a,t, ψ) are defined then:



 
B a,t, φ ta B a,t, φ ⇔ Pr(a,t, φ) > Pr(a,t, ψ)

We might not always have meaningful probabilities for all
propositions. For example, consider propositions of the form
“I believe that Jack believes that φ.” It is hard to get precise numbers for such statements. In such situations, we
might look at the ease of derivation of such statements given
a knowledge base Γ. Given two competing statements φ and
ψ, we can say one is more reasonable than the other if we can
easily derive one more than the other from Γ. This assumes
that we can derive φ and ψ from Γ. We assume we have a cost
function ρ : Proof 7→ R+ that lets us compute costs of proofs.
5 Something

similar to the system in [Halpern, 1990] that accounts for probabilities as statistical information or degrees of belief
can work.

There are many ways of specifying such functions. Possible candidates are length of the proof, time for computing the
proof, depth vs breadth of the proof, unique symbols used in
the proof etc. We leave this choice unspecified but any such
function could work here. Let `a,t denote provability w.r.t. to
agent a at time t.
Clause II. Defining 
If one of Pr(a,t, φ) and Pr(a,t, ψ) is not defined, but if Γ `a,t φ
and Γ `a,t ψ:

 


φ ta ψ ⇔ ρ Γ `a,t φ < ρ Γ `a,t ψ

Clauses I and II might not always hold. A more common
case could be when we cannot derive the propositions of interest from our background set of axioms Γ. For example,
if we are interested in the uncertainty values for statements
that we know are false, then it should be the case that they
be not derivable from our background set of axioms. In this
situation, we look at Γ and see what minimal changes we can
make to it to let us derive the proposition of interest. Trivially,
if we cannot derive φ from Γ, we can add it to Γ to derive it,
as Γ + φ ` φ. This is not desirable for two reasons.
First, simply adding to Γ might result in a contradiction. In
such cases we would be looking at removing a minimal set of
statements Λ from Γ. Second, we might prefer to add a more
simpler set of propositions Θ to Γ rather than φ itself to derive
φ. Recapping, we go from (1) to (2) below:
Γ 6` φ (1)
Γ ∪ Θ − Λ ` φ (2)

When we go from (1) to (2) we would like to modify the
background axioms as minimally as possible. Assume that
we have a similarity function π for sets of formulae. We then
choose Θ and Λ as given below (Con[S] denotes that S is consistent):
(
hΘ, Λi = arg min π(Γ, Γ ∪ Θ − Λ); such that
hΘ,Λi

Γ ∪ Θ − Λ ` φ; and


Con Γ ∪ Θ − Λ

Consider a statement such as “It rained last week” when
it did not actually rain last week, and another statement such
as “The moon is made of cheese.” Both statements denote
things that did not happen, but intuitively it seems that former should be more easier to accept from what we know than
the latter. There are many similarity measures which can help
convey this. Analogical reasoning is one such possible measure of similarity. If the new formulae are structurally similar
to existing formulae, then we might be more justified in accepting such formulae. For example, one such measure could
be the analogical measure used by us in [Licato et al., 2013].
Now we have the formal mechanism in place for defining
the final clause in our definition for our reasonableness. Let
δta (Γ, φ) be the distance between Γ and closest consistent set
under π that lets us prove φ:
(
δta (Γ, φ) ≡

min

hΘ,Λi

π Γ, Γ ∪ Θ − Λ



)

Γ ∪ Θ − Λ `ta ψ; and


Con Γ ∪ Θ − Λ

Clause III. Defining 
S1
If one of Pr(a,t, φ) and Pr(a,t, ψ) is not defined, and one of
Γ `a,t φ and Γ `a,t ψ does not hold, then

 h
i
φ ta ψ ⇔ δta (Γ, φ) < δta (Γ, ψ)

The final piece of S is inference rules for belief propagation
with uncertainty values. This is quite straightforward. Inferences propagate uncertainty values from the premises with
the lowest strength factor; and inferences happen only with
beliefs that are close in their uncertainty values, with maximum difference being parametrized by u, with default u = 2.
Inference Schemata for S
P(a,t1 , φ1 ), Γ ` t1 < t2
B5 (a,t2 , φ)

[RsP ]

Bs1 (a,t1 , φ1 ), . . . , Bsm (a,tm , φm ), {φ1 , . . . , φm } ` φ, Γ ` ti < t
Bmin(s1 ,...,sm ) (a,t, φ)
with max({s1 , . . . , sm }) − min({s1 , . . . , sm }) ≤ u

5

[RsB ]

Usage

In this section, we illustrate S by applying it solve problems of foundational interest such as the lottery paradox [Kyburg Jr, 1961, p. 197] and a toy version of a more real life
example, a murder mystery example (following in the traditions of logic pedagogy). Finally, we very briefly sketch
abstract scenarios in which S can be used to generate uncertainty values for counterfactual statements and to generate explanations for actions.

5.1

Paradoxes: Lottery Paradox

In the lottery paradox, we have a situation in which an agent a
comes to believe φ and ¬φ from a seemingly consistent set of
premises ΓL describing a lottery. Our solution to the paradox
is that the agent simply has different strengths of beliefs in
the proposition and its negation. We first go over the paradox
formalized in µC and then present the solution.
Let ΓL be a meticulous and perfectly accurate description
of a 1,000,000,000,000-ticket lottery, of which rational agent
a is fully apprised. Assume that from ΓL it can be proved
that either ticket 1 will win or ticket 2 will win or . . . or ticket
1,000,000,000,000 will win. Lets write this (exclusive) disjunction as follows (here ⊕ is an exclusive disjunction):
ΓL ` win(t1 ) ⊕ win(t2 ) ⊕ . . . ⊕ win(t1,000,000,000,000 )

The paradox has two strands of reasoning. The first strand
yields B(a, now, φ) and the second strand yields B(a, now, ¬φ)
with φ ≡ ∃t : win(t).
Strand 1: Since a believes all propositions in ΓL , a can then
deduce from this the belief that there is at least one ticket that
will win, a proposition represented as:



B a, now, ∃t : win t

Strand 2: From ΓL it can be proved that the probability of a
particular ticket ti winning is 10−12 .
i
i h 
h 


Pr a, now, win t1 = 10−12 ∧ Pr a, now, win t2 = 10−12
h 
i

∧ . . . ∧ Pr a, now, win t1T = 10−12

For the next step, note that the probability of ticket t1 winning is lower than, say, the probability that if you walk outside
a minute from now, you will be flattened on the spot by a door
from a 747 that falls from a jet of that type cruising at 35,000
feet. Since you, the reader, have the rational belief that death
won’t ensue if you go outside (and have this belief precisely
because you believe that the odds of your sudden demise in
this manner are vanishingly small), the inference to the rational belief on the part of a that t1 won’t win sails through —
and this of course works for each ticket. Hence we have as a
valid belief (though not derivable in µC from ΓL ):




B a, now, ¬win t1 ) ∧ B a, now, ¬win t2 ) ∧ . . .


∧ B a, now, ¬win t1T )

From RB and above, we get:


B a, now, ¬win t1 ) ∧ ¬win t2 ) ∧ . . . ∧ ¬win t1T )

Applying RB to the above and ΓL , we get:
S2



B a, now, ¬∃t : win(t)

The two strands are complete, and we have derived contradictory beliefs labeled S1 and S2 . Our solution consists of
two new uncertainty infused strands that result in beliefs of
sufficiently varying strengths that block inferences that could
combine them.
Strand 3: Assume that a is certain of all propositions in ΓL ,
then using RsB , we have:
S3


B5 a, now, ∃t : win(t)

Strand 4: Since Pr(a, now, win(ti )) < Pr(a, now, ¬win(ti )),
using Clause I and the strength factor definitions, we have
now that for all ti

B2 a, now, ¬win(ti )

Using the reasoning similar to that in Strand 2, we get:
S4



B2 a, now, ¬∃t : win(t)

Strands 3 and 4 resolve the paradox. Note that RsB cannot
be applied to S3 and S4 and churn out arbitrary propositions,
as the default value of the u parameter in RsB requires beliefs
to be no more than 2 levels apart. 

5.2

Application: Solving a Murder

We look at a toy example in which an agent s has to solve a
murder that happened at time t3 . s believes that either Alice
or Bob is the murderer. The agent knows that there is a gun
gun involved in the murder and that the owner of the gun at
t3 committed the murder. s also knows that Alice is the owner
of the gun initially at time t0 .

We may need non-trivial uncertainty values, but in this case,
Pr will assign a trivial value of 0 to both the propositions. We
can then look at closest consistent sets to Γ under δ:
Γ1 ` holds( f ,t 0 )
Γ2 ` holds(g,t 0 )

Clause III from the definition for reasonableness gives us:




B a,t, holds( f ,t 0 ) ta B a,t, holds(g,t 0 )

Presumption in Favor of Alice Being the Murderer

⇔
δta (Γ, Γ1 ) < δta (Γ, Γ2 )

From just these facts, the agent has some presumption for believing that Alice is the murderer.

Proof Sketch: All the above statements can be taken as certain beliefs B5 of s. For convenience, we consider the formulae directly without the belief operators.
In order to prove the above, we need to prove that it is
easier for the agent to derive that Alice is the murderer than
to derive that Alice is not the murderer. First, to prove the
former, the agent just has to assume that Alice’s ownership
of the gun did not change from t0 to t3 . Second, in order
for the agent to believe that Alice did not commit the murder but Bob committed it, the agent must be willing to admit that something happened to change Alice’s ownership of
the gun from time t0 to t3 that results in Bob owning the
gun. One possibility is that Alice simply sold the gun to
Bob. Both the scenarios are shown as proofs in the Slate
theorem proving workspace [Bringsjord et al., 2008] in the
Appendix. Figure 1 shows a proof modulo belief operators of
B(s, now, Murderer(Alice)) from Γ ∪ Θ1 and Figure 2 shows
a proof of B(s, now, ¬Murderer(Alice)) from Γ ∪ Θ2 .
If we assume that Θ1 and Θ2 exhaust the space of allowed
additions, then it easy to see how syntactic
measures of com
plexity will yield that δta Γ, Γ ∪ Θ1 < δta Γ, Γ ∪ Θ2 as Θ2 is
more complex than Θ1 . This lets us derive that s has some
presumption in favor of Murderer(Alice). 
What happens if the agent knows or has a belief with certainty that Alice’s ownership of the gun did not change from
t0 to t3 ?
Beyond Reasonable Doubt that Alice is the Murderer
If the agent is certain that Alice’s ownership of the gun did not
change from t0 till t3 , the agent has beyond reasonable doubt
that she is the murderer.

Proof Sketch: In this case we directly have that:
Γ ` B(s, now, Murderer(Alice))
Γ 6 ` ¬B(s, now, Murderer(Alice))
Γ 6 ` ¬B(s, now, ¬Murderer(Alice))

In order to flip the last two statements above, we need to modify Γ, but we can derive that Alice is the murderer without
any modifications, and since δta (Γ, Γ) = 0, it easier to believe
Alice is the murderer than to withhold that Alice is the murderer. 

5.3

Counterfactuals

At time t, assume that an agent a believes in a set of propositions Γ and is interested in propositions holds( f ,t 0 ) and
holds(g,t 0 ) with t 0 < t and:
Γ ` ¬holds( f ,t 0 ) ∧ ¬holds(g,t 0 )

5.4

Explanations

The definitions of the strength factors and reasonableness
above can be used to generate high-level schemas for explanations. These schemas can be used instead of simply presenting raw probability values to end-users. While we have
not fleshed out such explanation schemas, we illustrate one
possible schema. Say an agent performs an action α on the
basis of φ. In this case, the agent could generate an explanation that at the highest level simply says that it is more
reasonable for the agent to believe φ than for the agent to
believe in ¬φ. The agent could then further explain why it
was reasonable for it by using one of the three clauses in the
reasonableness definition.

6

Inference Algorithm Sketch

Describing the inference algorithm in detail is beyond the
scope of this paper, but we provide a high-level sketch here.6
Our proof calculus is simply an extension of standard firstorder proof calculus under different modal contexts. For example, if a believes that b believes in a set of propositions
Γ and Γ `FOL ψ, then a believes that b believes ψ. We
convert B (a,ta , B (b,tb , Q)) into the pure first-order formula
Q (context(a,ta , b,tb )) and use a first-order prover. The conversion process is a bit more nuanced as we have to handle
negations, properly handle substitutions of equalities, uncertainties and transform compound formulae within iterated beliefs.

7

Conclusion and Future Work

We have presented initial steps in building a system of uncertainty that is both probability and proof theory based that
could lend itself to (1) solving foundational problems; (2) being useful in applications; (3) generating uncertainty values
for counterfactuals; and (4) building understandable explanations.
Many challenges remain, some relatively easy and some
quite hard. Among the easy challenges are defining and experimenting with different candidates for Pr, ρ, π and δ. On
the more difficult side, we have to come up with tractable
computational mechanisms for computing the minhΘ,Λi in the
definition for δ. Also on the difficult side, is the challenge
of coming up efficient reasoning schemes. While we have an
exact inference algorithm, we believe that an approximate algorithm that selectively discards beliefs in a large knowledge
base during reasoning will be more useful.
6 More

details can be found here: https://goo.gl/2Vz2nJ

8

Acknowledgements

References

We are grateful to the Office of Naval Research for their funding of research that enabled the research presented in this paper.

A

Appendix: Slate Proofs

The figures below are vector graphics and can be zoomed to
more easily read the contents.


Figure 1: Alice is the murder: B s,t, Murderer(Alice)
Γ 1. Murderer(Alice) ∨ Murderer(Bob)
{Γ 1} Assume ✓

Γ 2. Murderer(Alice) → ¬Murderer(Bob)

Beliefs of s

{Γ 2} Assume ✓

Γ 3. Murderer(Bob) → ¬Murderer(Alice)
{Γ 3} Assume ✓

Γ 4. ∀x,t ((Holds(Owns(x,gun),t) ∧ holds(Owns(y,gun),t)) → (x = y))
{Γ 4} Assume ✓

Γ 5. Alice ≠ Bob

Γ 7. Initially(Owns(Alice,gun))

{Γ 5} Assume ✓

{Γ 7} Assume ✓

Γ 6. ∀x (Murderer(x) ↔ Holds(Owns(x,gun),t3))
{Γ 6} Assume ✓

Γ 8. ∀f,t ((Initially(f) ∧ ¬Clipped(t0,f,t)) → Holds(f,t))
{Γ 8} Assume ✓

Θ 1. ¬Clipped(t0,Owns(Alice,gun),t3)
{Θ 1} Assume ✓

⇥1

FOL ⊢ ✓

10. Murderer(Alice)
{Γ 1,Γ 2,Γ 3,Γ 4,Γ 5,Γ 6,Γ 7,Γ 8,Θ 1}



Figure 2: Alice is not the murder: B s,t, ¬Murderer(Alice)
Γ 1. Murderer(Alice) ∨ Murderer(Bob)
{Γ 1} Assume ✓

Γ 2. Murderer(Alice) → ¬Murderer(Bob)
{Γ 2} Assume ✓

Beliefs of s

Γ 3. Murderer(Bob) → ¬Murderer(Alice)
{Γ 3} Assume ✓

Γ 4. ∀x,t ((Holds(Owns(x,gun),t) ∧ holds(Owns(y,gun),t)) → (x = y))
{Γ 4} Assume ✓

Γ 5. Alice ≠ Bob
{Γ 5} Assume ✓

Γ 6. ∀x (Murderer(x) ↔ Holds(Owns(x,gun),t3))
{Γ 6} Assume ✓

Γ 7. Initially(Owns(Alice,gun))
{Γ 7} Assume ✓

Γ 8. ∀f,t ((Initially(f) ∧ ¬Clipped(t0,f,t)) → Holds(f,t))
{Γ 8} Assume ✓

Θ 1. ∀x,y,thing,t (Happens(Sold(x,y,thing),t) → (Clipped(t0,Owns(x,thing),t) ∧ Holds(Owns(y,thing),t)))
{Θ 1} Assume ✓

Θ 2. Happens(Sold(Alice,Bob,gun),t3)
{Θ 2} Assume ✓

FOL ⊢ ✓

11. Murderer(Bob) ∧ ¬Murderer(Alice)
{Γ 1,Γ 2,Γ 3,Γ 4,Γ 5,Γ 6,Γ 7,Γ 8,Θ 1,Θ 2}

⇥2

[Arkoudas and Bringsjord, 2008] Konstantine
Arkoudas
and
Selmer Bringsjord. Toward Formalizing Common-Sense Psychology: An Analysis of the False-Belief Task. In T.-B. Ho
and Z.-H. Zhou, editors, Proceedings of the Tenth Pacific Rim
International Conference on Artificial Intelligence (PRICAI
2008), number 5351 in Lecture Notes in Artificial Intelligence
(LNAI), pages 17–29. Springer-Verlag, 2008.
[Bringsjord et al., 2008] Selmer Bringsjord, Joshua Taylor, Andrew Shilliday, Micah Clark, and Konstantine Arkoudas. Slate:
An Argument-Centered Intelligent Assistant to Human Reasoners. In Floriana Grasso, Nancy Green, Rodger Kibble, and Chris
Reed, editors, Proceedings of the 8th International Workshop on
Computational Models of Natural Argument (CMNA 8), pages
1–10, Patras, Greece, July 21 2008. University of Patras.
[Bringsjord et al., 2014] Selmer Bringsjord, Naveen Sundar Govindarajulu, Daniel Thero, and Mei Si. Akratic Robots and the Computational Logic Thereof. In Proceedings of ETHICS • 2014
(2014 IEEE Symposium on Ethics in Engineering, Science, and
Technology), pages 22–29, Chicago, IL, 2014. IEEE Catalog
Number: CFP14ETI-POD.
[Chisholm, 1987] Roderick Chisholm. Theory of Knowledge 3rd
ed. Prentice-Hall, Englewood Cliffs, NJ, 1987.
[Demey et al., 2016] Lorenz Demey, Barteld Kooi, and Joshua
Sack. Logic and Probability. In Edward N. Zalta, editor,
The Stanford Encyclopedia of Philosophy. Metaphysics Research
Lab, Stanford University, winter 2016 edition, 2016.
[Gentzen, 1935] Gerhard Gentzen. Investigations into Logical Deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard
Gentzen, pages 68–131. North-Holland, Amsterdam, The Netherlands, 1935. This is an English version of the well-known 1935
German version.
[Govindarajulu and Bringsjord, 2017] Naveen Sundar Govindarajulu and Selmer Bringsjord. On Automating the Doctrine of
Double Effect. In Proceedings of the Twenty-Sixth International
Joint Conference on Artificial Intelligence (IJCAI 2017), 2017.
Preprint available at this url: https://arxiv.org/abs/1703.08922.
[Halpern, 1990] Joseph Y Halpern. An Analysis of First-order Logics of Probability. Artificial intelligence, 46(3):311–350, 1990.
[Kaye and Koehler, 1991] D. H. Kaye and Jonathan J. Koehler. Can
Jurors Understand Probabilistic Evidence? Journal of the Royal
Statistical Society. Series A (Statistics in Society), 154(1):75–81,
1991.
[Kyburg Jr, 1961] Henry E Kyburg Jr. Probability and the Logic
of Rational Belief. Wesleyan University Press, Middletown, CT,
1961.
[Licato et al., 2013] John Licato, Naveen Sundar Govindarajulu,
Selmer Bringsjord, Michael Pomeranz, and Logan Gittelson.
Analogico-Deductive Generation of Gödel’s First Incompleteness Theorem from the Liar Paradox. In Francesca Rossi, editor,
Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI–13), pages 1004–1009, Beijing, China,
2013. Morgan Kaufmann.
[Zalta, 1988] Edward N Zalta. Intensional Logic and the Metaphysics of Intentionality. MIT Press, Cambridge, MA, 1988.

