Transcript Overview of Non-Monotonic Reasoning

Belief Update, Planning
and the Fluent Calculus
Jacques Robin
Ontologies
Reasoning
Components
Agents
Simulations
Belief Update, Temporal Projection
and Planning
 Belief Update:
 CurrentBeliefAboutEnvironmentState x ExecutableAction 
BeliefAboutEnvironmentStateResultingFromActionExecution
 Temporal Projection:
 CurrentBeliefAboutEnvironmentState x ExecutableActionSequence 
BeliefAboutEnvironmentStateResultingFromActionSequenceExecution
If environment is partially observable, non-deterministic, multi-agent
adversarial or features exogenous actions (state changing non-agentive
events), it is impossible to determine the executability of an action
sequence (only the executability of the first action of the sequence can
be determined)
 Planning:
 CurrentBeliefAboutEnvironmentState x
EnvironmentStatePreferredByAgent  ExecutableActionSequence
The Fluent Calculus (FC):
Characteristics
 Language for Belief Update, Temporal Projection and Planning
Knowledge Representation
 Axiomatization with term reification of environment state changes
in Sorted Classical High-Order Logic (SCHOL)
 Sorts are type restrictions on atom and functional term arguments
 Environment-independent sorts, functions, predicates and foundational
axioms (one conjunctive SCHOL formula, only a single axiom is highorder)
 Environment-dependent sorts, functions, predicates and axioms (one
conjunctive Sorted Classical First-Order Logic (SCFOL))
 Reuses monotonic knowledge representation language (CFOL) to
formalize non-monotonic reasoning
 First language to fully solve the representational frame,
ramification and qualification problems
 Extends Situation Calculus with States
The FC: Environment
Formalization Process
1. Import the environment-independent FC sorts, functions, predicates
and foundational axioms
2. Define the environment-dependent (domain) sorts, functions,
predicates
3. Define the environment-dependent (domain) action precondition and
effect (state update) axioms (SCFOL formulas).
The FC Component Assembly
Simple FC: Belief Update, Temporal Project, Planning
Solving the Frame Problem
Disjunctive FC:
Solving the
Frame Problem
in NonDeterministic
Environments
Ramifying FC:
Solving the
Ramification
Problem
Qualifying FC:
Default
Reasoning
Solving the
Qualification
Problem
Concurrent FC:
Solving the
Frame Problem
in Concurrent
Environments
Meta FC:
Meta-Reasoning
about Agent’s own
Knowledge for
Boolean
Belief Revision
and Sensing
Action Planning
Plausibilistic FC:
Plausibilistic Belief
Revision
Full FC
Noise-Tolerant FC:
Solving the
Frame Problem
for Agents with
Noisy Sensors
Multi-Agent FC:
Reasoning about
Other Agents’
Knowledge and
Communicative
Action Planning
FLUX (FLUent eXecutor)
 Constraint Logic Programming Platform
 Provably correctly and efficiently implements the FC
 First platform to fully solves de inferential frame, ramification and
qualification problems
 FLUX architecture: two rule bases
 General Constraint Logic Programming
 Constraint Handling Rules
 Far more scalable than GOLOG’s situation calculus based platform
 Uses progressive planning with state (to avoid redundant execution of
reasoning steps of regressive planning from current situation back to the
initial one imposed by the situation calculus)
 Uses partial state representation
 Uses NAF under open-world semantics (!)
Simple FC: Abstract Syntax
Predicate
Symbol
SCFOL
Formula
SCFOL
Atom
predicate
arg 1..*
connective: CFOLConnectiveKind
arg 1..*
arg 1..*
{disjoint, complete}
SCFOL
Term
SCFOL
Quantifier Expression
{disjoint, complete}
quantfier: CFOLQuantifierKind
Non
Ground
Term
Ground
Term
Non
Functional
Term
Functional
Term
functor
Variable
Constant
Symbol
Domain
Predicate
Symbol
FC
Constant
Symbol
Domain
Constant
Symbol
Fluent FCFS
Sit FCFS
Action FCFS
State
FCCS
Sit
FCCS
FC
Function
Symbol


Function
Symbol
«enumeration»
CFOLConnectiveKind
Domain
Function
Symbol





State FCFS
FC
Predicate
Symbol
«enumeration»
CFOLConnectiveKind
Simple FC: Abstract Syntax
SCFOL
Formula
arg 1..*
arg 1..*
SCFOL
Atom
SCFOL
Term
connective: CFOLConnectiveKind
Domain
Atom
FC
Formula
Domain
Atom
FC
Atom
*
Pure State Formula
0..1
*
Holds
Atom
FC
Term
FC State Composition
Equality Atom
0..1
SitTerm
Action
Term
StateTerm
2
Fluent Term
2
Poss Axiom Formula
State Update Axiom Formula
Domain
Term
Simple FC Case Study:
Mail Delivering Robot
Simple FC: Foundational Axioms
Simple FC: Initial State
Representation
Simple FC:
Action Precondition Axioms
Simple FC: State Terms
and State Constraints
Simple FC: Fluent Collections
and State Update Axioms
(Belief Update)
Simple FC: Frame Problem Solution
Simple FC: Frame Problem Solution
Simple FC: Temporal Projection
as Deductive Entailment
Simple FC: Cause Abduction
as Deductive Entailment
Simple FC: Action Sequence Planning
as Deductive Entailment
FLUX: a CLP implementation of the FC
 Using the FC, agent reasoning can be implemented by a full CFOL
theorem prover
 Drawbacks of this approach:
 Full CFOL theorem provers are either only semi-automatic or not
scalable for large axioms and theorems
 FLUX approach:
 Rely on an efficient Constraint Logic Programming engine (e.g., ECLiPse
Prolog or Sictus Prolog)
 General Logic Program Rules
 Constraint Handling Rules
 Procedural Built-in Constraint Solving Libraries
FLUX: from SCFOL to GLP+CHR
 Partial state description as open Prolog list
CFOL atom z = f1 o ... o fn o z1, encoded as Z = [F1, ..., Fn | Z1]
 Non-Horn formula connectives as:
Additional predicates
 linked by appropriate integrity constraints
 defined using CHR,
 themselves defined using NAF and Prolog meta-programming as built-in
constraints
 e.g., Holds(f,z), encoded as notHolds(F,Z)
FLUX CHR Constraints
FLUX Built-in Predicates
Simple FLUX Programming Process
1.
2.
3.
4.
5.
6.
7.
8.
Define domain CHR using FLUX CHR
Define initial state Prolog facts
Define domain relation Prolog predicates
Define domain constraint by Prolog rules headed by FLUX predicate
consistent(Z)
Define preconditions of actions by Prolog rules headed by FLUX predicates
poss(A,Z) or not_poss(A,Z)
Define direct effects of actions by Prolog rules headed by FLUX predicates
state_update(Z1, A, Z2)
Define agent’s acting strategy by Prolog rules headed by FLUX predicate
do(As,Z1,Z2)
For planning queries, check executability of action sequences by NAF atoms
of the FLUX predicate non_executable(As,Z)
The Mail Delivery Robot
FLUX Program: CHR Program
The Mail Delivery Robot FLUX
Program: Initial State and
Domain Constraints
The Mail Delivery Robot FLUX Program:
Actions Preconditions
The Mail Delivery Robot FLUX
Program: Actions Direct Effects