diff --git a/encodings/pddl-sequential-horizon-boolean.lp b/encodings/pddl-sequential-horizon-boolean.lp
new file mode 100644
index 0000000..03c2605
--- /dev/null
+++ b/encodings/pddl-sequential-horizon-boolean.lp
@@ -0,0 +1,28 @@
+#const horizon=1.
+
+step(0..horizon).
+
+ precondition(Action,variable(Fluent),Value) :-  precondition(Action,                      variable(Fluent),value(Fluent,Value)).
+postcondition(Action,variable(Fluent),Value) :- postcondition(Action,effect(unconditional),variable(Fluent),value(Fluent,Value)).
+
+holds(variable(Fluent),0) :- initialState(variable(Fluent),value(Fluent,true)).
+
+ { occurs(Action,T) : action(Action) } = 1 :- step(T), T>0.
+
+:- occurs(Action,T), precondition(Action,Fluent,true), not holds(Fluent,T-1).
+:- occurs(Action,T), precondition(Action,Fluent,false),    holds(Fluent,T-1).
+
+caused(Fluent,T) :- occurs(Action,T), postcondition(Action,Fluent,true).
+
+holds(Fluent,T) :- caused(Fluent,T).
+holds(Fluent,T) :-  holds(Fluent,T-1), not occurs(Action,T) : postcondition(Action,Fluent,false); T<=horizon.
+
+goalAt(T) :-     holds(variable(Variable),T) : goal(variable(Variable), value(Variable,true));
+             not holds(variable(Variable),T) : goal(variable(Variable), value(Variable,false));
+	     T=horizon.
+
+ :- not goalAt(horizon).
+
+#show occurs/2.
+% #show holds/2.
+
diff --git a/encodings/pddl-sequential-incremental-boolean.lp b/encodings/pddl-sequential-incremental-boolean.lp
new file mode 100644
index 0000000..da03935
--- /dev/null
+++ b/encodings/pddl-sequential-incremental-boolean.lp
@@ -0,0 +1,31 @@
+#include <incmode>.
+
+#program base.
+
+ precondition(Action,variable(Fluent),Value) :-  precondition(Action,                      variable(Fluent),value(Fluent,Value)).
+postcondition(Action,variable(Fluent),Value) :- postcondition(Action,effect(unconditional),variable(Fluent),value(Fluent,Value)).
+
+holds(variable(Fluent),0) :- initialState(variable(Fluent),value(Fluent,true)).
+
+#program step(t).
+
+ { occurs(Action,t) : action(Action) } = 1.
+
+:- occurs(Action,t), precondition(Action,Fluent,true), not holds(Fluent,t-1).
+:- occurs(Action,t), precondition(Action,Fluent,false),    holds(Fluent,t-1).
+
+caused(Fluent,t) :- occurs(Action,t), postcondition(Action,Fluent,true).
+
+holds(Fluent,t) :- caused(Fluent,t).
+holds(Fluent,t) :-  holds(Fluent,t-1), not occurs(Action,t) : postcondition(Action,Fluent,false).
+
+#program check(t).
+
+goalAt(t) :-     holds(variable(Variable),t) : goal(variable(Variable), value(Variable,true));
+             not holds(variable(Variable),t) : goal(variable(Variable), value(Variable,false)).
+
+ :- not goalAt(t), query(t).
+
+#show occurs/2.
+% #show holds/2.
+
diff --git a/encodings/sas-sequential-incremental-multivalued-axioms-condeffects.lp b/encodings/sas-sequential-incremental-multivalued-axioms-condeffects.lp
new file mode 100644
index 0000000..5dad258
--- /dev/null
+++ b/encodings/sas-sequential-incremental-multivalued-axioms-condeffects.lp
@@ -0,0 +1,52 @@
+#include <incmode>.
+
+% Check feature requirements
+% :- requires(feature(actionCosts)).
+
+#program base.
+
+% Establish initial state
+holds(Variable, Value, 0) :- initialState(Variable, Value), not stateVariable(Variable).
+
+% Identify (head and) state variables
+headVariable(Rule,Variable) :- variable(Variable), axiomRule(Rule), postcondition(Rule,_,Variable,_).
+stateVariable(Variable)     :- headVariable(_,Variable).
+
+#program step(t). % t=1,2,...
+
+% Perform actions
+1 {occurs(Action, t) : action(Action)} 1.
+
+% Check preconditions
+:- occurs(Action, t), precondition(Action, Variable, Value), not holds(Variable, Value, t - 1).
+
+% Apply effects
+caused(Variable, Value, t) :- occurs(Action, t), postcondition(Action, Effect, Variable, Value),
+		  	      holds(Variable', Value', t) : precondition(Effect, Variable', Value').
+modified(Variable, t) :- caused(Variable, Value, t).
+
+holds(Variable, Value, t) :- caused(Variable, Value, t).
+holds(Variable, Value, t) :- holds(Variable, Value, t - 1), not modified(Variable, t).
+
+#program check(t). % t=0,1,...
+
+% Check that variables have unique values
+:- variable(Variable), {holds(Variable, Value, t) : contains(Variable, Value)} != 1.
+
+% Check mutexes
+:- mutexGroup(MutexGroup),  {holds(Variable, Value, t) : contains(MutexGroup, Variable, Value)} > 1.
+
+% Apply axioms
+derived(Variable, Value, t) :- axiomRule(Rule), postcondition(Rule,_,Variable,Value),
+		  	       holds(Variable', Value', t) : precondition(Rule, Variable', Value'), not headVariable(Rule,Variable').
+
+modified(Variable, t) :- derived(Variable, Value, t).
+
+holds(Variable, Value, t) :-      derived(Variable, Value, t), stateVariable(Variable).
+holds(Variable, Value, t) :- not modified(Variable,        t), stateVariable(Variable), initialState(Variable, Value).
+
+% Verify that goal is met
+:- query(t), goal(Variable, Value), not holds(Variable, Value, t).
+
+#show occurs/2.
+% #show holds/3.