Inference in the FO(C) Modelling Language
Bart Bogaerts, Joost Vennekens, Marc Denecker (KU Leuven)
Jan Van den Bussche (Hasselt University & transnational University of Limburg)
Goal (FO(C) project)
Develop a good modelling language for causality
Goal (This paper)
Study inference in FO(C)
Overview
- FO(C)
- Principles of Causation
- CP-Logic
- C-Log & FO(C)
- Inference
- Background: FO(ID)
-
Normal forms for FO(C)
- Relation with FO(ID)
-
Complexity of inference in FO(C)
Principles of Causation
- Universal causation: all events must be triggered by a causal law whose precondition is satisfied.
- Sufficient causation: if the precondition for a causal law is satisfied, then the event that it triggers must eventually happen.
- Independent causation: which event a causal law triggers is not influenced by other causal laws.
CP-Logic
Cause-effect relations
Turn(BigGear)←Pedal.(1)Turn(BigGear)←Turn(SmallGear).(2)Turn(SmallGear)←Turn(BigGear).(3)
{P}(1)→{P,T(B)}(3)→{P,T(B),T(S)}(2)→{P,T(B),T(S)}
Non-Determinism
Turn(SmallGear)OrChainBreaks←Turn(BigGear)
Branching of possibilities
C-Log
-
Extension of CP-Logic
- Motivation: many things are not naturally expressable in CP-Logic
-
Expressive
language for cause-effect relations
-
Non-deterministic
choice
-
Dynamic set of alternatives
-
Object creation
-
Arbitrary
nesting
-
...
Dynamic Choice
Selectx[φ(x)]:C
Lottery
Selectx[Plays(x)]:Rich(x)
In CP-Logic: only possible if Plays is known statically
Rich(Alice)OrRich(Bob)Or…
Nesting
Arbitrary nesting of effects
Lightning
(Selecth[House(h)]:(Allo[In(o,h)]:Broken(o))) ←Lightning
Object Creation
Newx:C
Existence of objects governed by causal rules
Mail Protocol
Allm,t[HitSend(m,t)]:Newp:Pack(p)AndOnCh(p,t)AndCont(p,m)
Summary: syntax
A
Causal Effect Expression (CEE) is one of the following:
(if
C,
C1,
C2 are CEEs,
φ a formula,
A an atom,
x a variable)
-
A
-
C←φ
-
C1AndC2
-
C1OrC2
-
Allx[φ]:C
-
Selectx[φ]:C
-
Newx:C
Formal semantics
Generalisation of instance-based semantics for D-LP
Based on Approximation Fixpoint Theory
FO(C)
First-order logic + C-Log
Overview (this paper)
- Background: FO(ID)
-
Normal forms for FO(C)
- Relation with FO(ID)
-
Complexity of inference in FO(C)
FO(ID)
- First-order logic
- Inductive Definitions
Inductive Definitions
Sets of rules of the form ∀x:P(ˉt)←φ
FO(ID) example
{∀x,y:R(x,y)←Edge(x,y)∀x,y:R(x,y)←∃z:R(x,z)∧R(z,y)}R(Start,End)
IDP
Knowledge Base System for FO(ID)
Goal: use IDP to perform inference on FO(C)
Normal Forms And Transformation
-
NestNF
-
Deterministic
- No Select, Or or
New expressions
-
DefNF
- Of the form
{Allˉx1[φ1]:P1(ˉt1)Allˉx2[φ2]:P2(ˉt2)⋯}
From FO(C) to NestNF
C subexpression of C1
C1 becomes
{C1[P(ˉx)/C]Allˉx[P(ˉx)]:C}
Example
Selecth[House(h)]:(Allo[In(o,h)]Broken(o)) ←Lightning
becomes
{Selecth[House(h)]:Hit(h)←LightningAllh[Hit(h)]:Allo[In(o,h)]Broken(o)}
From NestNF to Deterministic
Idea: explicitly represent choices
Example
Turn(SmallGear)OrChainBreaks←Turn(BigGear)
becomes
{Turn(SmallGear)←Turn(BigGear)∧FirstChainBreaks←Turn(BigGear)∧¬First}
Example
Selectx[Plays(x)]:Rich(x)
becomes
{Allx[Selected(x)]:Rich(x)]}∃1x:Selected(x)∀x:Selected(x)⇒Play(x)
From Deterministic to DefNF
Pushing All through And:
Allx[φ]:C1AndC2
becomes
{Allx[φ]:C1Allx[φ]:C2}
Model Expansion
NP-complete
Model Checking
NP-complete
FO(C) theory T: transform to ∃ˉP:T′, where T′ is an FO(ID) theory
Model checking of FO(C) = Model checking of ∃SO
(Unbounded) Endogenous Model Generation
Given: domain + interpretation for exogenous symbols
Find: model with larger domain (all new elements created by New)
Can decide every decidable class of finite structures
Implementation
Prototype of transformation, model expansion and model checking in IDP
References
(
B. Bogaerts, J. Vennekens, M. Denecker and J. Van den Bussche
)
-
Inference in the FO(C) Modelling Language
-
European Conference on Artificial Intelligence (ECAI),
2014.
-
15th International Workshop on Non-Monotonic Reasoning
,
2014
.
-
FO(C) and Related Modelling Paradigms
15th International Workshop on Non-Monotonic Reasoning,
2014.
-
FO(C): A Knowledge Representation Language of Causality
International Conference of Logic Programming (ICLP),
(Technical communication),
2014.