diff --git a/doc/output-format.md b/doc/output-format.md
index b6ebc74..9928c59 100644
--- a/doc/output-format.md
+++ b/doc/output-format.md
@@ -1,6 +1,15 @@
 # Output Format
 
-`plasp` 3 translates SAS and PDDL files into the same ASP fact format.
+`plasp` 3 translates SAS and PDDL files into a uniform ASP fact format.
+
+## Overview
+
+Essentially, `plasp`’s output format consists of *variables* that are modified by *actions* whose preconditions are fulfilled.
+
+`plasp`’s variables correspond to the multivalued variables in SAS.
+PDDL predicates are turned into Boolean variables to make the output format consistent.
+
+Actions are modeled exactly as PDDL actions and SAS operators.
 
 ## In a Nutshell
 
@@ -14,11 +23,7 @@ type(type(switch)).
 constant(constant(a)).
 has(constant(a), type(switch)).
 
-% introduces another switch "constant(a)"
-constant(constant(b)).
-has(constant(b), type(switch)).
-
-% declares a variable "variable(on(X))" for each switch X
+% declares a variable "variable(on(X))" for switches X
 variable(variable(on(X))) :- has(X, type(switch)).
 
 % the variable may be true or false
@@ -30,91 +35,55 @@ action(action(turnOn(X))) :- has(X, type(switch)).
 precondition(action(turnOn(X)), variable(on(X)), value(on(X), false)) :- has(X, type(switch)).
 postcondition(action(turnOn(X)), effect(0), variable(on(X)), value(on(X), true)) :- has(X, type(switch)).
 
-% declares the action "action(turnOff(X))", which requires switch X to be on and then turns it off
-action(action(turnOff(X))) :- has(X, type(switch)).
-precondition(action(turnOff(X)), variable(on(X)), value(on(X), true)) :- has(X, type(switch)).
-postcondition(action(turnOff(X)), effect(0), variable(on(X)), value(on(X), false)) :- has(X, type(switch)).
-
-% initially, switch a is off and switch b is on
+% initially, the switch is off
 initialState(variable(on(constant(a))), value(on(constant(a)), false)).
-initialState(variable(on(constant(b))), value(on(constant(b)), true)).
 
-% in the end, switch a should be on and switch b should be off
+% in the end, the switch should be on
 goal(variable(on(constant(a))), value(on(constant(a)), true)).
-goal(variable(on(constant(b))), value(on(constant(b)), false)).
 ```
 
-When translating SAS or PDDL problems, `plasp` structures the translated ASP facts into multiple sections, which are explained in the following.
+## Syntax and Semantics
 
-## Feature Requirements
+`plasp` structures the translated ASP facts into multiple sections, which are explained in the following.
 
-This section declares advanced features required by the input planning problem, such as conditional effects and axiom rules.
-
-Feature requirements may be used in meta encodings to warn about unsupported features.
-
-### Syntax
-
-syntax | description
--------|------------
-`requiresFeature(<feature name>).` | declares the feature `<feature name>` to be required by the input problem
-
-Currently, feature requirements are only recognized with SAS problems.
-`plasp` supports the following feature requirements:
-
-SAS feature | description
-------------|------------
-`actionCosts` | actions have associated costs
-`axiomRules` | immediate actions are used, which are executed as soon as the preconditions are satisfied
-`conditionalEffects` | some effects of an action may have additional conditions
-
-### Example
-
-The following specifies that the input problem has the two requirements `actionCosts` and `conditionalEffects`.
+### Feature Requirements
 
 ```prolog
-% requirements
-requiresFeature(actionCosts).
-requiresFeature(conditionalEffects).
+% declares a required feature
+requires(feature(<name>)).
 ```
 
-## Types
+`plasp` recognizes and declares advanced features used by the input problem, such as conditional effects and [axiom rules](#axiom-rules) (currently only SAS).
+See the [full list of supported features](feature-requirements.md) for more information.
 
-This section specifies all object types used by the problem (only with PDDL and if typing is enabled).
+The feature requirement predicates may be used in meta encodings to warn about unsupported features.
 
-### Syntax
-
-syntax | description
--------|------------
-`type(type(<type name>)).` | declares the type `type(<type name>)`
-
-### Example
-
-The following declares the type `type(block)` for later usage by the problem:
+### Types
 
 ```prolog
-% types
-type(type(block)).
+% declares a <type>
+type(type(<name>)).
+
+% specifies <object> to be of type type(<name>)
+has(<object>, type(<name>)).
 ```
 
-## Constants/Objects
+[Variables](#variables), [constants](#constants), and [objects](#objects) may be typed. Types are only available with PDDL and if typing is enabled.
 
-These two sections specify domain-specific (global) constants and problem-specific (local) objects (such as the blocks in a Blocks World puzzle).
-
-Constants and objects are not distinguished by `plasp`.
-
-### Syntax
-
-syntax | description
--------|------------
-`constant(constant(<constant name>)).` | declares the constant or object `constant(<constant name>)`
-`has(constant(<constant name>), type(<type name>)).` | declares constant or object `constant(<constant name>)` to be of [type](#type) `type(<type name>)`
-
-### Example
-
-The following declares a constant `constant(a)` of [type](#types) `type(block)`:
+### Variables
 
 ```prolog
-% objects
-constant(constant(a)).
-has(constant(a), type(block)).
+% declares a <variable>
+variable(variable(<name>)).
+
+% adds a <value> to the domain of a <variable>
+contains(<variable>, <value>).
 ```
+
+With SAS, variable names are numbers starting at 0, `variable(<number>)`.
+SAS variables are inherently multivalued, which results in two or more values of the form `value(<SAS predicate>, <bool>)` for each variable.
+
+With PDDL, Boolean variables are created from the PDDL predicates.
+Variables ared named after the PDDL predicates, `variable(<PDDL predicate>).`
+Each variable contains exactly two values (one true, one false) of the form `value(<PDDL predicate>, <bool>)`.
+Note that with PDDL, variables and values are named identically.