diff --git a/README.md b/README.md
index 1638658..ca6278a 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# plasp [![GitHub Release](https://img.shields.io/github/release/potassco/plasp.svg?maxAge=3600)](https://github.com/potassco/plasp/releases) [![Build Status](https://img.shields.io/travis/potassco/plasp/develop.svg?maxAge=3600&label=build (master))](https://travis-ci.org/potassco/plasp?branch=master) [![Build Status](https://img.shields.io/travis/potassco/plasp/develop.svg?maxAge=3600&label=build (develop))](https://travis-ci.org/potassco/plasp?branch=develop)
+# plasp [![GitHub Release](https://img.shields.io/github/release/potassco/plasp.svg?maxAge=3600)](https://github.com/potassco/plasp/releases) [![Build Status](https://img.shields.io/travis/potassco/plasp/master.svg?maxAge=3600&label=build (master))](https://travis-ci.org/potassco/plasp?branch=master) [![Build Status](https://img.shields.io/travis/potassco/plasp/develop.svg?maxAge=3600&label=build (develop))](https://travis-ci.org/potassco/plasp?branch=develop)
 
 > Translate PDDL to ASP
 
@@ -64,11 +64,12 @@ If you want to write your own meta encoding for `plasp`’s output, this [simple
 
 `plasp` requires `boost` and is built via CMake and a C++ compiler.
 
-See [building instructions](doc/building-instructions.md) for more details.
+See [building](doc/building.md) for more details.
 
 ## Contributors
 
 * [Patrick Lühne](https://www.luehne.de)
+* Martin Gebser (encodings)
 * Torsten Schaub (encodings)
 
 ### Earlier Versions
diff --git a/doc/building-instructions.md b/doc/building.md
similarity index 97%
rename from doc/building-instructions.md
rename to doc/building.md
index aafcaf7..8bc91b4 100644
--- a/doc/building-instructions.md
+++ b/doc/building.md
@@ -1,4 +1,4 @@
-# Building Instructions
+# Building
 
 `plasp` requires a C++14 compiler (preferrably GCC ≥ 6.1 or clang ≥ 3.8), the `boost` libraries (≥ 1.55), and CMake for building.
 
diff --git a/encodings/sequential-horizon.lp b/encodings/sequential-horizon.lp
new file mode 100644
index 0000000..135a22e
--- /dev/null
+++ b/encodings/sequential-horizon.lp
@@ -0,0 +1,36 @@
+#const horizon=1.
+
+% Check feature requirements
+:- requires(feature(actionCosts)).
+:- requires(feature(axiomRules)).
+:- requires(feature(conditionalEffects)).
+
+% Horizon, must be defined externally
+time(0..horizon).
+
+% Establish initial state
+holds(Variable, Value, 0) :- initialState(Variable, Value).
+
+% Perform actions
+1 {occurs(Action, T) : action(Action)} 1 :- time(T), T > 0.
+
+% Check preconditions
+:- occurs(Action, T), precondition(Action, Variable, Value), not holds(Variable, Value, T - 1), time(T), time(T - 1).
+
+% Apply effects
+caused(Variable, Value, T) :- occurs(Action, T), postcondition(Action, _, Variable, Value).
+modified(Variable, T) :- caused(Variable, Value, T).
+
+holds(Variable, Value, T) :- caused(Variable, Value, T), time(T).
+holds(Variable, Value, T) :- holds(Variable, Value, T - 1), not modified(Variable, T), time(T), time(T - 1).
+
+% Check that variables have unique values
+:- variable(Variable), not 1 {holds(Variable, Value, T) : contains(Variable, Value)} 1, time(T).
+
+% Check mutexes
+:- mutexGroup(MutexGroup), not {holds(Variable, Value, T) : contains(MutexGroup, Variable, Value)} 1, time(T).
+
+% Verify that goal is met
+:- goal(Variable, Value), not holds(Variable, Value, horizon).
+
+#show occurs/2.
diff --git a/encodings/strips/README.md b/encodings/strips/README.md
new file mode 100644
index 0000000..037ce05
--- /dev/null
+++ b/encodings/strips/README.md
@@ -0,0 +1,56 @@
+# Incremental STRIPS Planning Encodings
+
+This suite of incremental STRIPS planning encodings implements diverse methods.
+The included encoding files provide the following functionalities:
+
+## Encodings
+
+### [preprocess.lp](preprocess.lp): static analysis of potentially relevant actions
+
+* Parameters: `_closure` (default value: `3`)
+  * Value `1`: forward chaining of effects w.r.t. initial variable values
+  * Value `2`: backward regression of effects w.r.t. goal variable values
+  * Value `3`: both forward chaining and backward regression of effects
+  * Otherwise: off (simply take all actions as given)
+
+### [strips-incremental.lp](strips-incremental.lp): sequential and parallel planning encoding variants
+* Parameters: `_parallel` (default value: `0`)
+  * Value `1`: “forall” parallel actions that can be arranged in any sequence
+  * Value `2`: “exists” parallel actions that can be arranged in some sequence
+  * Otherwise: sequential actions
+
+### [redundancy.lp](redundancy.lp): enforcement of ‘redundant’ actions to constrain parallel plans
+* Remarks:
+  * Only relevant together with parallel actions
+  * Encoded constraints seem rather ineffective though
+  * Heavy space overhead in combination with “exists” parallel actions
+
+### [postprocess.lp](postprocess.lp): plan feasibility checking and conversion to sequential plan
+
+## Usage Examples
+
+Some example invocations (using `clingo` 5.1.0) are as follows:
+
+```bash
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp -c _closure=0
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp -c _closure=1
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp -c _closure=2
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp -c _parallel=1
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp -c _parallel=2
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp -c _parallel=1 redundancy.lp
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp -c _parallel=2 redundancy.lp
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp --outf=1 | grep -A1 -e "ANSWER" | tail -n1 | clingo - postprocess.lp <(plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl)
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp --outf=1 -c _parallel=1 | grep -A1 -e "ANSWER" | tail -n1 | clingo - postprocess.lp <(plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl)
+
+plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl | clingo - preprocess.lp strips-incremental.lp --outf=1 -c _parallel=2 | grep -A1 -e "ANSWER" | tail -n1 | clingo - postprocess.lp <(plasp ../../instances/PDDL/ipc-2000-elevator-m10-strips/domain.pddl ../../instances/PDDL/ipc-2000-elevator-m10-strips/problem-04-00.pddl)
+```
diff --git a/encodings/strips/postprocess.lp b/encodings/strips/postprocess.lp
new file mode 100644
index 0000000..3c24305
--- /dev/null
+++ b/encodings/strips/postprocess.lp
@@ -0,0 +1,58 @@
+% Convert a plan (possibly with parallel actions), given by atoms over occurs/2,
+% to a sequential plan, expressed by atoms over sequence/2
+
+time(T) :- occurs(A,T).
+time    :- time(T).
+
+:- goal(X,V), not initialState(X,V), not time.
+
+last(T2) :- time, T2 = #max{T1 : time(T1)}.
+
+offset(T2,M)    :- time(T2), M = #count{A,T1 : occurs(A,T1), T1 < T2}.
+finish(T,M+N)   :- offset(T,M), N = #count{A : occurs(A,T)}.
+index(T,M+1..N) :- offset(T,M), finish(T,N).
+
+postcondition(A,X,V) :- postcondition(A,E,X,V), occurs(A,T).
+postcondition(A,X)   :- postcondition(A,X,V).
+
+before(A1,A2,T) :- occurs(A1,T), occurs(A2,T), A1 != A2,
+                   precondition(A1,X,V), postcondition(A2,X), not postcondition(A2,X,V).
+
+order(A1,A2,T) :- occurs(A1,T), occurs(A2,T), A1 < A2, A <= A1 : occurs(A,T), A < A2.
+first(A2,T)    :- occurs(A2,T), #false : order(A1,A2,T).
+
+undone(A,T,M) :- occurs(A,T), offset(T,M).
+undone(A,T,N) :- undone(A,T,N-1), select(A1,T,N), A != A1, index(T,N+1).
+
+done(A,T,N) :- select(A,T,N).
+done(A,T,N) :- done(A,T,N-1), index(T,N).
+
+:- finish(T,N), occurs(A,T), not done(A,T,N).
+
+hold(X,V,0) :- initialState(X,V).
+hold(X,V,N) :- select(A,T,N), postcondition(A,X,V).
+hold(X,V,N) :- select(A,T,N), hold(X,V,N-1), not postcondition(A,X).
+
+:- last(T), finish(T,N), goal(X,V), not hold(X,V,N).
+
+hold(X,N) :- hold(X,V,N).
+
+:- hold(X,N), #count{V : hold(X,V,N)} > 1.
+
+preconditions(A,T,N) :- undone(A,T,N), hold(X,V,N) : precondition(A,X,V).
+applicable(A,T,N)    :- preconditions(A,T,N), done(A1,T,N) : before(A1,A,T).
+
+inapplicable(A,T,N) :- done(A,T,N), index(T,N+1).
+inapplicable(A,T,N) :- undone(A,T,N), precondition(A,X,V1), hold(X,V2,N), V1 != V2.
+inapplicable(A,T,N) :- undone(A1,T,N), before(A1,A,T).
+
+continue(A2,T,N) :- order(A1,A2,T), inapplicable(A1,T,N), first(A1,T).
+continue(A2,T,N) :- order(A1,A2,T), inapplicable(A1,T,N), continue(A1,T,N).
+
+select(A,T,N+1) :- applicable(A,T,N), first(A,T).
+select(A,T,N+1) :- applicable(A,T,N), continue(A,T,N).
+
+% DISPLAY PART
+
+#show.
+#show sequence(A,N) : select(A,T,N).
diff --git a/encodings/strips/preprocess.lp b/encodings/strips/preprocess.lp
new file mode 100644
index 0000000..bd60246
--- /dev/null
+++ b/encodings/strips/preprocess.lp
@@ -0,0 +1,48 @@
+% Constant '_closure' to (de)activate analysis of potentially relevant actions
+% - value '1': forward chaining of effects w.r.t. initial variable values
+% - value '2': backward regression of effects w.r.t. goal variable values
+% - value '3': both forward chaining and backward regression of effects
+% - otherwise: off
+
+#const _closure = 3.
+
+% Check feature requirements
+
+:- requires(feature(actionCosts)).
+:- requires(feature(axiomRules)).
+:- requires(feature(conditionalEffects)).
+
+% Basic redundancy check for actions
+
+postcondition(A,X,V) :- postcondition(A,E,X,V).
+
+has_condition(A,X,0) :- action(A), precondition(A,X,V).
+has_condition(A,X,1) :- action(A), postcondition(A,X,V).
+
+inconsistent(A) :- has_condition(A,X,P),
+                   #count{V : precondition(A,X,V), P = 0;
+                          V : postcondition(A,X,V), P = 1} > 1.
+consistent(A)   :- action(A), not inconsistent(A).
+irredundant(A)  :- consistent(A), postcondition(A,X,V), not precondition(A,X,V).
+
+% Forward chaining of effects w.r.t. initial variable values
+
+feasible(X,V) :- initialState(X,V).
+feasible(X,V) :- possible(A), postcondition(A,X,V).
+
+possible(A) :- irredundant(A), feasible(X,V) : precondition(A,X,V).
+possible(A) :- irredundant(A), _closure != 1, _closure != 3.
+
+:- goal(X,V), not feasible(X,V).
+
+% Backward regression of effects w.r.t. goal variable values
+
+produce(X,V) :- goal(X,V), not initialState(X,V).
+produce(X,V) :- active(A), precondition(A,X,V), not initialState(X,V).
+produce(X,V) :- persist(X,V), active(A), has_condition(A,X,1), not postcondition(A,X,V).
+
+persist(X,V) :- goal(X,V), initialState(X,V).
+persist(X,V) :- active(A), precondition(A,X,V), initialState(X,V).
+
+active(A) :- possible(A), postcondition(A,X,V), produce(X,V).
+active(A) :- possible(A), _closure != 2, _closure != 3.
diff --git a/encodings/strips/redundancy.lp b/encodings/strips/redundancy.lp
new file mode 100644
index 0000000..ef67f92
--- /dev/null
+++ b/encodings/strips/redundancy.lp
@@ -0,0 +1,33 @@
+% Additional rules for enforcing the inclusion of parallel actions in plans,
+% whenever such 'redundant' actions are compatible with states and other actions
+
+compatible(A,A1) :- active(A), active(A1), A != A1, _parallel = 2,
+                    not diverge(A,A1), not diverge(A1,A).
+compatible(A)    :- compatible(A,A1).
+
+disable(A,A1,A2) :- disable(A1,A2), compatible(A,A1), compatible(A,A2).
+disabled(A,A2)   :- disable(A,A1,A2).
+disabled(A,A2)   :- disable(A,A2).
+
+#program step(t).
+
+defeated(A,t) :- active(A), postcondition(A,X,V), fluent(X), not holds(X,V,t),
+                 _parallel = 1 : _parallel != 2.
+
+defeated(A,t) :- _parallel = 1, active(A), precondition(A,X,V), not holds(X,V,t-1).
+defeated(A,t) :- _parallel = 1, active(A), precondition(A,X,V), not holds(X,V,t).
+defeated(A,t) :- _parallel = 1, active(A), postcondition(A,X,V), not precondition(A,X,V),
+                 single(X,t).
+
+proceed(A,X,V,t) :- compatible(A), holds(X,V,t-1), scope(X,V).
+proceed(A,X,V,t) :- compatible(A,A1), occurs(A1,t), perform(A,A1,t),
+                    postcondition(A1,X,V), scope(X,V), not precondition(A1,X,V).
+
+perform(A,A1,t) :- disabled(A,A1), not occurs(A1,t).
+perform(A,A1,t) :- compatible(A,A1),
+                   proceed(A,X,V,t) : precondition(A1,X,V); perform(A,A2,t) : disable(A,A1,A2).
+
+defeated(A,t) :- compatible(A), precondition(A,X,V), not proceed(A,X,V,t).
+defeated(A,t) :- compatible(A), disable(A,A2), not perform(A,A2,t).
+
+:- active(A), not occurs(A,t), not defeated(A,t), _parallel = 1 : _parallel != 2.
diff --git a/encodings/strips/strips-incremental.lp b/encodings/strips/strips-incremental.lp
new file mode 100644
index 0000000..8f26060
--- /dev/null
+++ b/encodings/strips/strips-incremental.lp
@@ -0,0 +1,104 @@
+% Constant '_parallel' to enable parallel actions
+% - value '1': "forall" parallel actions that can be arranged in any sequence
+% - value '2': "exists" parallel actions that can be arranged in some sequence
+% - otherwise: sequential actions
+
+#const _parallel = 0.
+
+#include <incmode>.
+
+% BASE PROGRAM
+
+% Define auxiliary predicates for actions w.r.t. parallel mode
+
+diverge(A1,A2,X) :- active(A1), active(A2), A1 < A2, postcondition(A1,X,V),
+                    has_condition(A2,X,1), not postcondition(A2,X,V),
+                    _parallel = 1 : _parallel != 2.
+diverge(A1,A2)   :- diverge(A1,A2,X).
+
+exclude(A1,A2) :- diverge(A1,A2), precondition(A1,X,V), _parallel = 1,
+                  has_condition(A2,X,0), not precondition(A2,X,V).
+
+disable(A1,A2) :- active(A1), active(A2), A1 != A2, postcondition(A1,X,V),
+                  has_condition(A2,X,0), not precondition(A2,X,V),
+                  _parallel = 2, not diverge(A1,A2), not diverge(A2,A1).
+
+scope(X,V) :- active(A), precondition(A,X,V), _parallel = 2.
+
+% Define relevant fluents w.r.t. parallel mode
+
+fluent(X,V) :- produce(X,V).
+fluent(X,V) :- persist(X,V).
+fluent(X,V) :- initialState(X,V), fluent(X).
+fluent(X,V) :- active(A), postcondition(A,X,V), fluent(X).
+fluent(X)   :- fluent(X,V).
+fluent(X)   :- diverge(A1,A2,X), not exclude(A1,A2).
+
+% Define unsubsumed mutexes
+
+mutex(G,X) :- mutexGroup(G), contains(G,X,V), fluent(X,V).
+mutex(G)   :- mutexGroup(G), #count{X : mutex(G,X)} > 1.
+
+% Define initial state
+
+holds(X,V,0) :- initialState(X,V), fluent(X).
+
+:- fluent(X), #count{V : holds(X,V,0)} > 1.
+:- mutex(G), #count{X,V : holds(X,V,0), contains(G,X,V)} > 1.
+
+% STEP PROGRAM
+
+#program step(t).
+
+% Generate successor state
+
+1 {holds(X,V,t) : fluent(X,V)} 1 :- fluent(X).
+
+:- mutex(G), #count{X,V : holds(X,V,t), contains(G,X,V)} > 1.
+
+change(X,t) :- holds(X,V,t-1), not holds(X,V,t).
+
+% Generate actions
+
+1 {occurs(A,t) : active(A)}.
+
+:- occurs(A,t), postcondition(A,X,V), fluent(X), not holds(X,V,t).
+
+effect(X,t) :- occurs(A,t), postcondition(A,X,V), fluent(X), not precondition(A,X,V).
+
+:- change(X,t), not effect(X,t).
+
+% Checks w.r.t. parallel mode
+
+:- _parallel != 1, _parallel != 2, #count{A : occurs(A,t)} > 1.
+
+:- _parallel != 2, occurs(A,t), precondition(A,X,V), not holds(X,V,t-1).
+
+:- _parallel = 1, occurs(A,t), precondition(A,X,V), not has_condition(A,X,1), not holds(X,V,t).
+
+single(X,t) :- occurs(A,t), precondition(A,X,V), _parallel = 1,
+               has_condition(A,X,1), not postcondition(A,X,V).
+
+:- single(X,t), #count{A : occurs(A,t), postcondition(A,X,V), not precondition(A,X,V)} > 1.
+
+proceed(X,V,t) :- holds(X,V,t-1), scope(X,V).
+proceed(X,V,t) :- occurs(A,t), postcondition(A,X,V), scope(X,V), not precondition(A,X,V),
+                  perform(A,t).
+
+perform(A1,t) :- active(A1), _parallel = 2, not occurs(A1,t).
+perform(A1,t) :- active(A1), _parallel = 2,
+                 proceed(X,V,t) : precondition(A1,X,V); perform(A2,t) : disable(A1,A2).
+
+:- _parallel = 2, active(A), not perform(A,t).
+
+% CHECK PROGRAM
+
+#program check(t).
+
+% Check goal conditions
+
+:- query(t), goal(X,V), not holds(X,V,t).
+
+% DISPLAY PART
+
+#show occurs/2.