diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..57872d0
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/vendor/
diff --git a/.scrutinizer.yml b/.scrutinizer.yml
new file mode 100644
index 0000000..06e2fe7
--- /dev/null
+++ b/.scrutinizer.yml
@@ -0,0 +1,57 @@
+# inherit the next configuration down the chain
+inherit: true
+
+filter:
+  paths:
+    - 'src/*'
+
+before_commands:
+  - 'composer install --no-interaction --no-scripts'
+
+tools:
+  php_mess_detector:
+    config:
+      code_size_rules:
+        cyclomatic_complexity: true
+        npath_complexity: true
+        excessive_method_length: true
+        excessive_class_length: true
+        excessive_parameter_list: true
+        excessive_public_count: true
+        too_many_fields: true
+        too_many_methods: true
+        excessive_class_complexity: true
+      design_rules:
+        number_of_class_children: true
+        depth_of_inheritance: true
+        coupling_between_objects: true
+      unused_code_rules:
+        unused_local_variable: true
+        unused_private_method: true
+        unused_formal_parameter: true
+      naming_rules:
+        short_variable: false
+        long_variable: true
+        short_method: true
+        boolean_method_name: true
+      controversial_rules: ~
+  php_cs_fixer:
+    config:
+      level: all
+  php_analyzer:
+    config:
+      suspicious_code: { enabled: true, overriding_parameter: true }
+      verify_php_doc_comments: { enabled: true }
+      loops_must_use_braces: { enabled: true }
+      simplify_boolean_return: { enabled: true }
+      phpunit_checks: { enabled: true }
+      reflection_fixes: { enabled: true }
+      use_statement_fixes: { enabled: true, order_alphabetically: true }
+  php_code_sniffer:
+    config:
+      standard: PSR2
+  sensiolabs_security_checker: true
+  php_loc: true
+  php_pdepend: true
+  php_sim: true
+  php_changetracking: true
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 0000000..e2b00e1
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,27 @@
+language: php
+
+php:
+  - 5.6
+  - 5.5
+  - hhvm
+
+env:
+  global:
+    - SYMFONY_ENV=test
+
+cache:
+  directories:
+    - $HOME/.composer
+
+matrix:
+  fast_finish: true
+  allow_failures:
+    - php: 5.6
+    - php: hhvm
+
+before_script:
+  - composer selfupdate
+  - composer install --no-interaction --no-scripts
+
+script:
+  - ./vendor/bin/phpunit
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..3ada3d7
--- /dev/null
+++ b/README.md
@@ -0,0 +1,6 @@
+Propositional Calculus
+======================
+
+Implementation of a Propositional Calculus in PHP.
+
+Based on the book [Artificial Intelligence - foundations of computational agents](http://artint.info) chapter [5 Propositions and Inference](http://artint.info/html/ArtInt_100.html).
diff --git a/composer.json b/composer.json
new file mode 100644
index 0000000..138a19a
--- /dev/null
+++ b/composer.json
@@ -0,0 +1,25 @@
+{
+    "name": "fieg/propositional-calculus",
+    "license": "MIT",
+    "description": "Implementation of a Propositional Calculus in PHP",
+    "type": "library",
+    "keywords": ["artificial", "intelligence", "propositional", "calculus"],
+    "homepage": "https://github.com/fieg/csp",
+    "authors": [
+      {
+        "name": "fieg",
+        "email": "jeroen@webcreate.nl"
+      }
+    ],
+    "minimum-stability": "stable",
+    "require": {
+    },
+    "require-dev": {
+        "phpunit/phpunit": "~4.1"
+    },
+    "autoload": {
+      "psr-4": {
+        "Fieg\\PC\\": "src/Fieg/PC/"
+      }
+    }
+}
diff --git a/composer.lock b/composer.lock
new file mode 100644
index 0000000..9d3efad
--- /dev/null
+++ b/composer.lock
@@ -0,0 +1,720 @@
+{
+    "_readme": [
+        "This file locks the dependencies of your project to a known state",
+        "Read more about it at http://getcomposer.org/doc/01-basic-usage.md#composer-lock-the-lock-file"
+    ],
+    "hash": "9a9c76223e534a04ca91faffbdc7fc4f",
+    "packages": [
+
+    ],
+    "packages-dev": [
+        {
+            "name": "phpunit/php-code-coverage",
+            "version": "2.0.8",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/php-code-coverage.git",
+                "reference": "58401826c8cfc8fd689b60026e91c337df374bca"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/php-code-coverage/zipball/58401826c8cfc8fd689b60026e91c337df374bca",
+                "reference": "58401826c8cfc8fd689b60026e91c337df374bca",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3",
+                "phpunit/php-file-iterator": "~1.3.1",
+                "phpunit/php-text-template": "~1.2.0",
+                "phpunit/php-token-stream": "~1.2.2",
+                "sebastian/environment": "~1.0.0",
+                "sebastian/version": "~1.0.3"
+            },
+            "require-dev": {
+                "ext-xdebug": ">=2.1.4",
+                "phpunit/phpunit": "~4.0.14"
+            },
+            "suggest": {
+                "ext-dom": "*",
+                "ext-xdebug": ">=2.2.1",
+                "ext-xmlwriter": "*"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "2.0.x-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "include-path": [
+                ""
+            ],
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sb@sebastian-bergmann.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "Library that provides collection, processing, and rendering functionality for PHP code coverage information.",
+            "homepage": "https://github.com/sebastianbergmann/php-code-coverage",
+            "keywords": [
+                "coverage",
+                "testing",
+                "xunit"
+            ],
+            "time": "2014-05-26 14:55:24"
+        },
+        {
+            "name": "phpunit/php-file-iterator",
+            "version": "1.3.4",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/php-file-iterator.git",
+                "reference": "acd690379117b042d1c8af1fafd61bde001bf6bb"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/php-file-iterator/zipball/acd690379117b042d1c8af1fafd61bde001bf6bb",
+                "reference": "acd690379117b042d1c8af1fafd61bde001bf6bb",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3"
+            },
+            "type": "library",
+            "autoload": {
+                "classmap": [
+                    "File/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "include-path": [
+                ""
+            ],
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sb@sebastian-bergmann.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "FilterIterator implementation that filters files based on a list of suffixes.",
+            "homepage": "https://github.com/sebastianbergmann/php-file-iterator/",
+            "keywords": [
+                "filesystem",
+                "iterator"
+            ],
+            "time": "2013-10-10 15:34:57"
+        },
+        {
+            "name": "phpunit/php-text-template",
+            "version": "1.2.0",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/php-text-template.git",
+                "reference": "206dfefc0ffe9cebf65c413e3d0e809c82fbf00a"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/php-text-template/zipball/206dfefc0ffe9cebf65c413e3d0e809c82fbf00a",
+                "reference": "206dfefc0ffe9cebf65c413e3d0e809c82fbf00a",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3"
+            },
+            "type": "library",
+            "autoload": {
+                "classmap": [
+                    "Text/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "include-path": [
+                ""
+            ],
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sb@sebastian-bergmann.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "Simple template engine.",
+            "homepage": "https://github.com/sebastianbergmann/php-text-template/",
+            "keywords": [
+                "template"
+            ],
+            "time": "2014-01-30 17:20:04"
+        },
+        {
+            "name": "phpunit/php-timer",
+            "version": "1.0.5",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/php-timer.git",
+                "reference": "19689d4354b295ee3d8c54b4f42c3efb69cbc17c"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/php-timer/zipball/19689d4354b295ee3d8c54b4f42c3efb69cbc17c",
+                "reference": "19689d4354b295ee3d8c54b4f42c3efb69cbc17c",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3"
+            },
+            "type": "library",
+            "autoload": {
+                "classmap": [
+                    "PHP/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "include-path": [
+                ""
+            ],
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sb@sebastian-bergmann.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "Utility class for timing",
+            "homepage": "https://github.com/sebastianbergmann/php-timer/",
+            "keywords": [
+                "timer"
+            ],
+            "time": "2013-08-02 07:42:54"
+        },
+        {
+            "name": "phpunit/php-token-stream",
+            "version": "1.2.2",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/php-token-stream.git",
+                "reference": "ad4e1e23ae01b483c16f600ff1bebec184588e32"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/php-token-stream/zipball/ad4e1e23ae01b483c16f600ff1bebec184588e32",
+                "reference": "ad4e1e23ae01b483c16f600ff1bebec184588e32",
+                "shasum": ""
+            },
+            "require": {
+                "ext-tokenizer": "*",
+                "php": ">=5.3.3"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "1.2-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "PHP/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "include-path": [
+                ""
+            ],
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sb@sebastian-bergmann.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "Wrapper around PHP's tokenizer extension.",
+            "homepage": "https://github.com/sebastianbergmann/php-token-stream/",
+            "keywords": [
+                "tokenizer"
+            ],
+            "time": "2014-03-03 05:10:30"
+        },
+        {
+            "name": "phpunit/phpunit",
+            "version": "4.1.1",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/phpunit.git",
+                "reference": "1d6b554732382879045e11c56decd4be76130720"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/phpunit/zipball/1d6b554732382879045e11c56decd4be76130720",
+                "reference": "1d6b554732382879045e11c56decd4be76130720",
+                "shasum": ""
+            },
+            "require": {
+                "ext-dom": "*",
+                "ext-json": "*",
+                "ext-pcre": "*",
+                "ext-reflection": "*",
+                "ext-spl": "*",
+                "php": ">=5.3.3",
+                "phpunit/php-code-coverage": "~2.0",
+                "phpunit/php-file-iterator": "~1.3.1",
+                "phpunit/php-text-template": "~1.2",
+                "phpunit/php-timer": "~1.0.2",
+                "phpunit/phpunit-mock-objects": "~2.1",
+                "sebastian/comparator": "~1.0",
+                "sebastian/diff": "~1.1",
+                "sebastian/environment": "~1.0",
+                "sebastian/exporter": "~1.0",
+                "sebastian/version": "~1.0",
+                "symfony/yaml": "~2.0"
+            },
+            "suggest": {
+                "phpunit/php-invoker": "~1.1"
+            },
+            "bin": [
+                "phpunit"
+            ],
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "4.1.x-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "include-path": [
+                "",
+                "../../symfony/yaml/"
+            ],
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sebastian@phpunit.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "The PHP Unit Testing framework.",
+            "homepage": "http://www.phpunit.de/",
+            "keywords": [
+                "phpunit",
+                "testing",
+                "xunit"
+            ],
+            "time": "2014-05-24 10:48:51"
+        },
+        {
+            "name": "phpunit/phpunit-mock-objects",
+            "version": "2.1.0",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/phpunit-mock-objects.git",
+                "reference": "da0eb04d8ee95ec2898187e407e519c118d3d27c"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/phpunit-mock-objects/zipball/da0eb04d8ee95ec2898187e407e519c118d3d27c",
+                "reference": "da0eb04d8ee95ec2898187e407e519c118d3d27c",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3",
+                "phpunit/php-text-template": "~1.2"
+            },
+            "require-dev": {
+                "phpunit/phpunit": "~4.1"
+            },
+            "suggest": {
+                "ext-soap": "*"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "2.1.x-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "include-path": [
+                ""
+            ],
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sb@sebastian-bergmann.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "Mock Object library for PHPUnit",
+            "homepage": "https://github.com/sebastianbergmann/phpunit-mock-objects/",
+            "keywords": [
+                "mock",
+                "xunit"
+            ],
+            "time": "2014-05-02 07:04:11"
+        },
+        {
+            "name": "sebastian/comparator",
+            "version": "1.0.0",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/comparator.git",
+                "reference": "f7069ee51fa9fb6c038e16a9d0e3439f5449dcf2"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/comparator/zipball/f7069ee51fa9fb6c038e16a9d0e3439f5449dcf2",
+                "reference": "f7069ee51fa9fb6c038e16a9d0e3439f5449dcf2",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3",
+                "sebastian/diff": "~1.1",
+                "sebastian/exporter": "~1.0"
+            },
+            "require-dev": {
+                "phpunit/phpunit": "~4.1"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "1.0.x-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sebastian@phpunit.de",
+                    "role": "lead"
+                },
+                {
+                    "name": "Jeff Welch",
+                    "email": "whatthejeff@gmail.com"
+                },
+                {
+                    "name": "Volker Dusch",
+                    "email": "github@wallbash.com"
+                },
+                {
+                    "name": "Bernhard Schussek",
+                    "email": "bschussek@2bepublished.at"
+                }
+            ],
+            "description": "Provides the functionality to compare PHP values for equality",
+            "homepage": "http://www.github.com/sebastianbergmann/comparator",
+            "keywords": [
+                "comparator",
+                "compare",
+                "equality"
+            ],
+            "time": "2014-05-02 07:05:58"
+        },
+        {
+            "name": "sebastian/diff",
+            "version": "1.1.0",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/diff.git",
+                "reference": "1e091702a5a38e6b4c1ba9ca816e3dd343df2e2d"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/diff/zipball/1e091702a5a38e6b4c1ba9ca816e3dd343df2e2d",
+                "reference": "1e091702a5a38e6b4c1ba9ca816e3dd343df2e2d",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "1.1-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sebastian@phpunit.de",
+                    "role": "lead"
+                },
+                {
+                    "name": "Kore Nordmann",
+                    "email": "mail@kore-nordmann.de"
+                }
+            ],
+            "description": "Diff implementation",
+            "homepage": "http://www.github.com/sebastianbergmann/diff",
+            "keywords": [
+                "diff"
+            ],
+            "time": "2013-08-03 16:46:33"
+        },
+        {
+            "name": "sebastian/environment",
+            "version": "1.0.0",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/environment.git",
+                "reference": "79517609ec01139cd7e9fded0dd7ce08c952ef6a"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/environment/zipball/79517609ec01139cd7e9fded0dd7ce08c952ef6a",
+                "reference": "79517609ec01139cd7e9fded0dd7ce08c952ef6a",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3"
+            },
+            "require-dev": {
+                "phpunit/phpunit": "4.0.*@dev"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "1.0.x-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sebastian@phpunit.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "Provides functionality to handle HHVM/PHP environments",
+            "homepage": "http://www.github.com/sebastianbergmann/environment",
+            "keywords": [
+                "Xdebug",
+                "environment",
+                "hhvm"
+            ],
+            "time": "2014-02-18 16:17:19"
+        },
+        {
+            "name": "sebastian/exporter",
+            "version": "1.0.1",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/exporter.git",
+                "reference": "1f9a98e6f5dfe0524cb8c6166f7c82f3e9ae1529"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/exporter/zipball/1f9a98e6f5dfe0524cb8c6166f7c82f3e9ae1529",
+                "reference": "1f9a98e6f5dfe0524cb8c6166f7c82f3e9ae1529",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3"
+            },
+            "require-dev": {
+                "phpunit/phpunit": "4.0.*@dev"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "1.0.x-dev"
+                }
+            },
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sebastian@phpunit.de",
+                    "role": "lead"
+                },
+                {
+                    "name": "Jeff Welch",
+                    "email": "whatthejeff@gmail.com"
+                },
+                {
+                    "name": "Volker Dusch",
+                    "email": "github@wallbash.com"
+                },
+                {
+                    "name": "Adam Harvey",
+                    "email": "aharvey@php.net"
+                },
+                {
+                    "name": "Bernhard Schussek",
+                    "email": "bschussek@2bepublished.at"
+                }
+            ],
+            "description": "Provides the functionality to export PHP variables for visualization",
+            "homepage": "http://www.github.com/sebastianbergmann/exporter",
+            "keywords": [
+                "export",
+                "exporter"
+            ],
+            "time": "2014-02-16 08:26:31"
+        },
+        {
+            "name": "sebastian/version",
+            "version": "1.0.3",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/sebastianbergmann/version.git",
+                "reference": "b6e1f0cf6b9e1ec409a0d3e2f2a5fb0998e36b43"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/sebastianbergmann/version/zipball/b6e1f0cf6b9e1ec409a0d3e2f2a5fb0998e36b43",
+                "reference": "b6e1f0cf6b9e1ec409a0d3e2f2a5fb0998e36b43",
+                "shasum": ""
+            },
+            "type": "library",
+            "autoload": {
+                "classmap": [
+                    "src/"
+                ]
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "license": [
+                "BSD-3-Clause"
+            ],
+            "authors": [
+                {
+                    "name": "Sebastian Bergmann",
+                    "email": "sebastian@phpunit.de",
+                    "role": "lead"
+                }
+            ],
+            "description": "Library that helps with managing the version number of Git-hosted PHP projects",
+            "homepage": "https://github.com/sebastianbergmann/version",
+            "time": "2014-03-07 15:35:33"
+        },
+        {
+            "name": "symfony/yaml",
+            "version": "v2.5.0",
+            "target-dir": "Symfony/Component/Yaml",
+            "source": {
+                "type": "git",
+                "url": "https://github.com/symfony/Yaml.git",
+                "reference": "b4b09c68ec2f2727574544ef0173684281a5033c"
+            },
+            "dist": {
+                "type": "zip",
+                "url": "https://api.github.com/repos/symfony/Yaml/zipball/b4b09c68ec2f2727574544ef0173684281a5033c",
+                "reference": "b4b09c68ec2f2727574544ef0173684281a5033c",
+                "shasum": ""
+            },
+            "require": {
+                "php": ">=5.3.3"
+            },
+            "type": "library",
+            "extra": {
+                "branch-alias": {
+                    "dev-master": "2.5-dev"
+                }
+            },
+            "autoload": {
+                "psr-0": {
+                    "Symfony\\Component\\Yaml\\": ""
+                }
+            },
+            "notification-url": "https://packagist.org/downloads/",
+            "license": [
+                "MIT"
+            ],
+            "authors": [
+                {
+                    "name": "Fabien Potencier",
+                    "email": "fabien@symfony.com",
+                    "homepage": "http://fabien.potencier.org",
+                    "role": "Lead Developer"
+                },
+                {
+                    "name": "Symfony Community",
+                    "homepage": "http://symfony.com/contributors"
+                }
+            ],
+            "description": "Symfony Yaml Component",
+            "homepage": "http://symfony.com",
+            "time": "2014-05-16 14:25:18"
+        }
+    ],
+    "aliases": [
+
+    ],
+    "minimum-stability": "stable",
+    "stability-flags": [
+
+    ],
+    "platform": [
+
+    ],
+    "platform-dev": [
+
+    ]
+}
diff --git a/phpunit.xml.dist b/phpunit.xml.dist
new file mode 100644
index 0000000..1a2086b
--- /dev/null
+++ b/phpunit.xml.dist
@@ -0,0 +1,27 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- http://www.phpunit.de/manual/current/en/appendixes.configuration.html -->
+<phpunit
+        backupGlobals               = "false"
+        backupStaticAttributes      = "false"
+        colors                      = "true"
+        convertErrorsToExceptions   = "true"
+        convertNoticesToExceptions  = "true"
+        convertWarningsToExceptions = "true"
+        processIsolation            = "false"
+        stopOnFailure               = "false"
+        syntaxCheck                 = "false"
+        bootstrap                   = "tests/bootstrap.php">
+
+  <testsuites>
+    <testsuite name="Test Suite">
+      <directory>tests</directory>
+    </testsuite>
+  </testsuites>
+
+  <filter>
+    <whitelist>
+      <directory suffix=".php">src/</directory>
+    </whitelist>
+  </filter>
+</phpunit>
diff --git a/src/Fieg/PC/CompoundProposition.php b/src/Fieg/PC/CompoundProposition.php
new file mode 100644
index 0000000..e3694db
--- /dev/null
+++ b/src/Fieg/PC/CompoundProposition.php
@@ -0,0 +1,43 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC;
+
+abstract class CompoundProposition extends Proposition
+{
+    protected $propositions;
+
+    public function __construct(array $args)
+    {
+        foreach($args as $arg) {
+            if (!$arg instanceof Proposition) {
+                throw new \InvalidArgumentException('arg is not a valid proposition');
+            }
+
+            $this->addProposition($arg);
+        }
+    }
+
+    /**
+     * @param Proposition $proposition
+     * @return $this
+     */
+    public function addProposition(Proposition $proposition)
+    {
+        $this->propositions[] = $proposition;
+
+        return $this;
+    }
+
+    /**
+     * @return mixed
+     */
+    public function getPropositions()
+    {
+        return $this->propositions;
+    }
+}
diff --git a/src/Fieg/PC/KnowledgeBase.php b/src/Fieg/PC/KnowledgeBase.php
new file mode 100644
index 0000000..620ad9e
--- /dev/null
+++ b/src/Fieg/PC/KnowledgeBase.php
@@ -0,0 +1,135 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC;
+
+use Fieg\PC\Proof\DeductionBottomUpStrategy;
+use Fieg\PC\Proof\ProofStrategyInterface;
+use Fieg\PC\Proposition\AndX;
+use Fieg\PC\Proposition\Atomic;
+
+class KnowledgeBase
+{
+    protected $propositions;
+    protected $proofStrategy;
+
+    /**
+     * Constructor.
+     *
+     * @param ProofStrategyInterface $proofStrategy a default proof strategy
+     */
+    public function __construct(ProofStrategyInterface $proofStrategy = null)
+    {
+        if (null === $proofStrategy) {
+            $proofStrategy = new DeductionBottomUpStrategy();
+        }
+
+        $this->proofStrategy = $proofStrategy;
+    }
+
+    /**
+     * @param Proposition $proposition
+     */
+    public function addProposition(Proposition $proposition)
+    {
+        $this->propositions[] = $proposition;
+    }
+
+    /**
+     * @param Proposition[] $propositions
+     */
+    public function addPropositions(array $propositions)
+    {
+        foreach($propositions as $proposition) {
+            $this->addProposition($proposition);
+        }
+    }
+
+    /**
+     * @return mixed
+     */
+    public function getPropositions()
+    {
+        return $this->propositions;
+    }
+
+    /**
+     * @param string $name
+     * @param null|Proposition[] $propositions
+     * @return Atomic|null
+     */
+    public function getAtomByName($name, array $propositions = null)
+    {
+        if (null === $propositions) {
+            $propositions = $this->getPropositions();
+        }
+
+        foreach($propositions as $proposition) {
+            if ($proposition instanceof Atomic && $name === $proposition->getName()) {
+                return $proposition;
+            } elseif ($proposition instanceof CompoundProposition) {
+                $result = $this->getAtomByName($name, $proposition->getPropositions());
+                if (null !== $result) {
+                    return $result;
+                }
+            }
+        }
+
+        return null;
+    }
+
+    /**
+     * @param ProofStrategyInterface $strategy
+     * @throws \InvalidArgumentException
+     * @return Proposition[]
+     */
+    public function proof(ProofStrategyInterface $strategy = null)
+    {
+        if (null === $strategy) {
+            $strategy = $this->proofStrategy;
+        }
+
+        return $strategy->proof($this->getPropositions());
+    }
+
+    /**
+     * @param Proposition $body
+     * @return bool
+     * @throws \InvalidArgumentException
+     */
+    public function query(Proposition $body)
+    {
+        if (!$body instanceof Atomic && !$body instanceof AndX) {
+            throw new \InvalidArgumentException(sprintf('Body can only be an instance of Atomic or AndX, %s given', get_class($body)));
+        }
+
+        if ($body instanceof AndX) {
+            if (false === $body->isDefiniteClauseBody()) {
+                throw new \InvalidArgumentException(
+                    'Given AndX is not a valid body because it contains compound propositions, '.
+                    'it should only contain atomic propositions'
+                );
+            }
+        }
+
+        if ($body instanceof Atomic) {
+            $proof = $this->proof();
+
+            return in_array($body, $proof);
+        } else if ($body instanceof AndX) {
+            foreach($body->getPropositions() as $proposition) {
+                if (false === $this->query($proposition)) {
+                    return false;
+                }
+            }
+
+            return true;
+        }
+
+        return false;
+    }
+}
diff --git a/src/Fieg/PC/Proof/DeductionBottomUpStrategy.php b/src/Fieg/PC/Proof/DeductionBottomUpStrategy.php
new file mode 100644
index 0000000..0c3a5d9
--- /dev/null
+++ b/src/Fieg/PC/Proof/DeductionBottomUpStrategy.php
@@ -0,0 +1,89 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC\Proof;
+
+use Fieg\PC\CompoundProposition;
+use Fieg\PC\Proposition;
+
+class DeductionBottomUpStrategy implements ProofStrategyInterface
+{
+    public function proof(array $propositions)
+    {
+        $propositions = array_filter($propositions, array($this, 'isDefiniteClause'));
+
+        $c = array();
+
+        while(false !== $h = $this->_proof($propositions, $c)) {
+            $c[] = $h;
+        }
+
+        return $c;
+    }
+
+    /**
+     * @param Proposition[] $clauses
+     * @param array $c
+     * @return bool|\Fieg\PC\Proposition
+     */
+    protected function _proof(array &$clauses, array $c)
+    {
+        foreach($clauses as $i => $clause) {
+            $h = $clause;
+            $b = array();
+
+            if ($clause instanceof Proposition\Implies) {
+                $h = $clause->getHead();
+                $body = $clause->getBody();
+
+                if ($body instanceof CompoundProposition) {
+                    $b = $body->getPropositions();
+                } else {
+                    $b = array($body);
+                }
+            }
+
+            if (!in_array($h, $c) && $this->all_in_array($b, $c)) {
+                unset($clauses[$i]);
+
+                return $h;
+            }
+        }
+
+        return false;
+    }
+
+    /**
+     * @param array $needles
+     * @param array $haystack
+     * @return bool
+     */
+    protected function all_in_array(array $needles, array $haystack)
+    {
+        foreach($needles as $needle) {
+            if (false === in_array($needle, $haystack)) {
+                return false;
+            }
+        }
+
+        return true;
+    }
+
+    /**
+     * Indicates if a proposition is a definite clause
+     *
+     * @param Proposition $p
+     * @return bool
+     */
+    public function isDefiniteClause(Proposition $p)
+    {
+        return (
+            $p instanceof Proposition\Atomic
+            || ($p instanceof Proposition\Implies && $p->getHead() instanceof Proposition\Atomic)
+        );
+    }
+}
diff --git a/src/Fieg/PC/Proof/ProofStrategyInterface.php b/src/Fieg/PC/Proof/ProofStrategyInterface.php
new file mode 100644
index 0000000..f4b3df5
--- /dev/null
+++ b/src/Fieg/PC/Proof/ProofStrategyInterface.php
@@ -0,0 +1,13 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC\Proof;
+
+interface ProofStrategyInterface 
+{
+    public function proof(array $propositions);
+}
diff --git a/src/Fieg/PC/Proposition.php b/src/Fieg/PC/Proposition.php
new file mode 100644
index 0000000..b56fc4d
--- /dev/null
+++ b/src/Fieg/PC/Proposition.php
@@ -0,0 +1,12 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC;
+
+abstract class Proposition
+{
+}
diff --git a/src/Fieg/PC/Proposition/AndX.php b/src/Fieg/PC/Proposition/AndX.php
new file mode 100644
index 0000000..af2d39f
--- /dev/null
+++ b/src/Fieg/PC/Proposition/AndX.php
@@ -0,0 +1,36 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC\Proposition;
+
+use Fieg\PC\CompoundProposition;
+use Fieg\PC\Proposition;
+
+class AndX extends CompoundProposition
+{
+    public function __toString()
+    {
+        $propositions = array_map('strval', $this->propositions);
+
+        $retval = implode(' ^ ', $propositions);
+
+        return '(' . $retval . ')';
+    }
+
+    public function isDefiniteClauseBody()
+    {
+        foreach($this->getPropositions() as $proposition) {
+            if (!$proposition instanceof Atomic) {
+                return false;
+            }
+        }
+
+        return true;
+    }
+}
+
+
diff --git a/src/Fieg/PC/Proposition/Atomic.php b/src/Fieg/PC/Proposition/Atomic.php
new file mode 100644
index 0000000..f2261cd
--- /dev/null
+++ b/src/Fieg/PC/Proposition/Atomic.php
@@ -0,0 +1,33 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC\Proposition;
+
+use Fieg\PC\Proposition;
+
+class Atomic extends Proposition
+{
+    protected $name;
+
+    public function __construct($name)
+    {
+        $this->name = $name;
+    }
+
+    /**
+     * @return mixed
+     */
+    public function getName()
+    {
+        return $this->name;
+    }
+
+    public function __toString()
+    {
+        return (string) $this->name;
+    }
+}
diff --git a/src/Fieg/PC/Proposition/Implies.php b/src/Fieg/PC/Proposition/Implies.php
new file mode 100644
index 0000000..ca10029
--- /dev/null
+++ b/src/Fieg/PC/Proposition/Implies.php
@@ -0,0 +1,52 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC\Proposition;
+
+use Fieg\PC\CompoundProposition;
+use Fieg\PC\Proposition;
+
+class Implies extends CompoundProposition
+{
+    protected $head;
+    protected $body;
+
+    public function __construct(Proposition $p, Proposition $q)
+    {
+        $this->head = $p;
+        $this->body = $q;
+
+        $this->addProposition($p);
+        $this->addProposition($q);
+    }
+
+    /**
+     * @return \Fieg\PC\Proposition
+     */
+    public function getHead()
+    {
+        return $this->head;
+    }
+
+    /**
+     * @return \Fieg\PC\Proposition
+     */
+    public function getBody()
+    {
+        return $this->body;
+    }
+
+    public function __toString()
+    {
+        $head = (string) $this->head;
+        $body = (string) $this->body;
+
+        return sprintf('%s <- %s', $head, $body);
+    }
+}
+
+
diff --git a/src/Fieg/PC/Proposition/NotX.php b/src/Fieg/PC/Proposition/NotX.php
new file mode 100644
index 0000000..dea4a95
--- /dev/null
+++ b/src/Fieg/PC/Proposition/NotX.php
@@ -0,0 +1,30 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC\Proposition;
+
+use Fieg\PC\CompoundProposition;
+use Fieg\PC\Proposition;
+
+class NotX extends CompoundProposition
+{
+    public function __construct(Proposition $p)
+    {
+        $this->propositions = array($p);
+    }
+
+    public function __toString()
+    {
+        $propositions = array_map('strval', $this->propositions);
+
+        $retval = implode('', $propositions);
+
+        return '¬(' . $retval . ')';
+    }
+}
+
+
diff --git a/src/Fieg/PC/Proposition/OrX.php b/src/Fieg/PC/Proposition/OrX.php
new file mode 100644
index 0000000..d09c761
--- /dev/null
+++ b/src/Fieg/PC/Proposition/OrX.php
@@ -0,0 +1,22 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC\Proposition;
+
+use Fieg\PC\CompoundProposition;
+
+class OrX extends CompoundProposition
+{
+    public function __toString()
+    {
+        $propositions = array_map('strval', $this->propositions);
+
+        $retval = implode(' v ', $propositions);
+
+        return '(' . $retval . ')';
+    }
+}
diff --git a/src/Fieg/PC/PropositionBuilder.php b/src/Fieg/PC/PropositionBuilder.php
new file mode 100644
index 0000000..4a59988
--- /dev/null
+++ b/src/Fieg/PC/PropositionBuilder.php
@@ -0,0 +1,93 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+namespace Fieg\PC;
+
+use Fieg\PC\Proposition\AndX;
+use Fieg\PC\Proposition\Atomic;
+use Fieg\PC\Proposition\Implies;
+use Fieg\PC\Proposition\NotX;
+use Fieg\PC\Proposition\OrX;
+
+class PropositionBuilder
+{
+    /**
+     * Atom index
+     *
+     * Contains atoms that were created using this builder
+     *
+     * @var Atomic[]
+     */
+    protected $atoms = array();
+
+    /**
+     * Returns an atom. When called twice with the same name
+     * the first atom that was created is returned.
+     *
+     * @param string $name
+     * @return Atomic
+     */
+    public function atom($name)
+    {
+        if (false === isset($this->atoms[$name])) {
+            $this->atoms[$name] = new Atomic($name);
+        }
+
+        return $this->atoms[$name];
+    }
+
+    /**
+     * @return Atomic[]
+     */
+    public function getAtoms()
+    {
+        return $this->atoms;
+    }
+
+    /**
+     * @param $p
+     * @param $q
+     * @return Implies
+     */
+    public function implies($p, $q)
+    {
+        return new Implies($p, $q);
+    }
+
+    /**
+     * @param $args
+     * @return AndX
+     */
+    public function andX($args)
+    {
+        $args = func_get_args();
+
+        return new AndX($args);
+    }
+
+    /**
+     * @param $args
+     * @return OrX
+     */
+    public function orX($args)
+    {
+        $args = func_get_args();
+
+        return new OrX($args);
+    }
+
+    /**
+     * @param $p
+     * @return NotX
+     */
+    public function notX($p)
+    {
+        return new NotX($p);
+    }
+}
+
+
diff --git a/tests/Fieg/PC/KnowledgeBaseTest.php b/tests/Fieg/PC/KnowledgeBaseTest.php
new file mode 100644
index 0000000..e818c74
--- /dev/null
+++ b/tests/Fieg/PC/KnowledgeBaseTest.php
@@ -0,0 +1,155 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+use Fieg\PC\Proposition\Atomic;
+use Fieg\PC\Proof\DeductionBottomUpStrategy;
+
+class KnowledgeBaseTest extends \PHPUnit_Framework_TestCase
+{
+    public function testBuilder()
+    {
+        $pb = new \Fieg\PC\PropositionBuilder();
+
+        $a = new Atomic('a');
+        $b = new Atomic('b');
+        $c = new Atomic('c');
+        $d = new Atomic('d');
+        $e = new Atomic('e');
+        $f = new Atomic('f');
+        $g = new Atomic('g');
+
+        $kb = new \Fieg\PC\KnowledgeBase();
+        $kb->addProposition($pb->implies($a, $pb->andX($b, $c)));
+        $kb->addProposition($b);
+        $kb->addProposition($pb->andX($b, $c));
+        $kb->addProposition(
+            $pb->implies(
+                $pb->orX(
+                    $pb->notX($a),
+                    $pb->andX($b, $c)
+                ),
+                $pb->orX(
+                    $pb->andX(
+                        $d,
+                        $pb->notX($e)
+                    ),
+                    $f
+                )
+            )
+        );
+
+        $expected = array(
+            'a <- (b ^ c)',
+            'b',
+            '(b ^ c)',
+            '(¬(a) v (b ^ c)) <- ((d ^ ¬(e)) v f)',
+        );
+
+        $this->assertEquals($expected, array_map('strval', $kb->getPropositions()));
+    }
+
+    public function testProof()
+    {
+        $pb = new \Fieg\PC\PropositionBuilder();
+
+        $live_l1 = new Atomic('live_l1');
+        $live_w0 = new Atomic('live_w0');
+        $live_w1 = new Atomic('live_w1');
+        $live_w2 = new Atomic('live_w2');
+        $live_w3 = new Atomic('live_w3');
+        $up_s1 = new Atomic('up_s1');
+        $up_s2 = new Atomic('up_s2');
+        $down_s1 = new Atomic('down_s1');
+        $down_s2 = new Atomic('down_s2');
+
+        $kb = new \Fieg\PC\KnowledgeBase();
+
+        $props = array();
+        $props[] = $pb->implies($live_l1, $live_w0);
+        $props[] = $pb->implies($live_w0, $pb->andX($live_w1, $up_s2));
+        $props[] = $pb->implies($live_w0, $pb->andX($live_w2, $down_s2));
+        $props[] = $pb->implies($live_w1, $pb->andX($live_w3, $up_s1));
+        $props[] = $pb->implies($live_w2, $pb->andX($live_w3, $down_s1));
+
+        $props[] = $live_l1;
+        $props[] = $down_s1;
+        $props[] = $live_w3;
+
+        $kb->addPropositions($props);
+
+        $conclusion = $kb->proof(new DeductionBottomUpStrategy());
+
+        $expected = array(
+            $live_l1,
+            $down_s1,
+            $live_w3,
+            $live_w2,
+        );
+
+        $this->assertEquals($expected, $conclusion);
+    }
+
+    public function testQuery()
+    {
+        $pb = new \Fieg\PC\PropositionBuilder();
+
+        $kb = new \Fieg\PC\KnowledgeBase();
+
+        // atomic clauses
+        $kb->addProposition($pb->atom('light_l1'));
+        $kb->addProposition($pb->atom('light_l2'));
+        $kb->addProposition($pb->atom('ok_l1'));
+        $kb->addProposition($pb->atom('ok_l2'));
+        $kb->addProposition($pb->atom('ok_cb1'));
+        $kb->addProposition($pb->atom('ok_cb2'));
+        $kb->addProposition($pb->atom('live_outside'));
+
+        // rules
+        $kb->addProposition($pb->implies($pb->atom('live_l1'), $pb->atom('live_w0')));
+        $kb->addProposition($pb->implies($pb->atom('live_w0'), $pb->andX($pb->atom('live_w1'), $pb->atom('up_s2'))));
+        $kb->addProposition($pb->implies($pb->atom('live_w0'), $pb->andX($pb->atom('live_w2'), $pb->atom('down_s2'))));
+        $kb->addProposition($pb->implies($pb->atom('live_w1'), $pb->andX($pb->atom('live_w3'), $pb->atom('up_s1'))));
+        $kb->addProposition($pb->implies($pb->atom('live_w2'), $pb->andX($pb->atom('live_w3'), $pb->atom('down_s1'))));
+        $kb->addProposition($pb->implies($pb->atom('live_l2'), $pb->atom('live_w4')));
+        $kb->addProposition($pb->implies($pb->atom('live_w4'), $pb->andX($pb->atom('live_w3'), $pb->atom('up_s3'))));
+        $kb->addProposition($pb->implies($pb->atom('live_p1'), $pb->atom('live_w3')));
+        $kb->addProposition($pb->implies($pb->atom('live_w3'), $pb->andX($pb->atom('live_w5'), $pb->atom('ok_cb1'))));
+        $kb->addProposition($pb->implies($pb->atom('live_p2'), $pb->atom('live_w6')));
+        $kb->addProposition($pb->implies($pb->atom('live_w6'), $pb->andX($pb->atom('live_w5'), $pb->atom('ok_cb2'))));
+        $kb->addProposition($pb->implies($pb->atom('live_w5'), $pb->atom('live_outside')));
+        $kb->addProposition($pb->implies($pb->atom('lit_l1'), $pb->andX($pb->atom('light_l1'), $pb->atom('live_l1'), $pb->atom('ok_l1'))));
+        $kb->addProposition($pb->implies($pb->atom('lit_l2'), $pb->andX($pb->atom('light_l2'), $pb->atom('live_l2'), $pb->atom('ok_l2'))));
+
+        // observations
+        $kb->addProposition($pb->atom('down_s1'));
+        $kb->addProposition($pb->atom('up_s2'));
+        $kb->addProposition($pb->atom('up_s3'));
+
+        extract($pb->getAtoms());
+
+        /** @var $light_l1 \Fieg\PC\Proposition */
+        $this->assertTrue($kb->query($light_l1));
+        $this->assertFalse($kb->query($pb->atom('light_l6'))); // light_l6 is not in KB
+        $this->assertTrue($kb->query($lit_l2));
+    }
+
+    public function testGetAtomByName()
+    {
+        $pb = new \Fieg\PC\PropositionBuilder();
+
+        $kb = new \Fieg\PC\KnowledgeBase();
+        $kb->addProposition($pb->atom('ok_cb1'));
+        $kb->addProposition($pb->atom('ok_cb2'));
+        $kb->addProposition($pb->implies($pb->atom('live_l1'), $pb->atom('live_w0')));
+        $kb->addProposition($pb->implies($pb->atom('live_w0'), $pb->andX($pb->atom('live_w1'), $pb->atom('up_s2'))));
+        $kb->addProposition($pb->implies($pb->atom('live_w0'), $pb->andX($pb->atom('live_w2'), $pb->atom('down_s2'))));
+
+        $this->assertSame($pb->atom('live_w0'), $kb->getAtomByName('live_w0'));
+        $this->assertSame($pb->atom('ok_cb1'), $kb->getAtomByName('ok_cb1'));
+        $this->assertNull($kb->getAtomByName('atom_does_not_exist'));
+    }
+}
diff --git a/tests/Fieg/PC/PropositionBuilderTest.php b/tests/Fieg/PC/PropositionBuilderTest.php
new file mode 100644
index 0000000..7bddfbe
--- /dev/null
+++ b/tests/Fieg/PC/PropositionBuilderTest.php
@@ -0,0 +1,51 @@
+<?php
+
+/*
+ * @author Jeroen Fiege <jeroen@webcreate.nl>
+ * @copyright Webcreate (http://webcreate.nl)
+ */
+
+class PropositionBuilderTest extends \PHPUnit_Framework_TestCase
+{
+    public function testBuilder()
+    {
+        $pb = new \Fieg\PC\PropositionBuilder();
+
+        $a = new \Fieg\PC\Proposition\Atomic('a');
+        $b = new \Fieg\PC\Proposition\Atomic('b');
+
+        $this->assertInstanceOf('Fieg\PC\Proposition\Implies', $pb->implies($a, $b));
+        $this->assertInstanceOf('Fieg\PC\Proposition\AndX', $pb->andX($a, $b));
+        $this->assertInstanceOf('Fieg\PC\Proposition\OrX', $pb->orX($a, $b));
+        $this->assertInstanceOf('Fieg\PC\Proposition\Atomic', $pb->atom('thingy'));
+        $this->assertInstanceOf('Fieg\PC\Proposition\NotX', $pb->notX($a));
+    }
+
+    public function testAtomUniquness()
+    {
+        $pb = new \Fieg\PC\PropositionBuilder();
+
+        $atom = $pb->atom('light_1');
+        $atom2 = $pb->atom('light_1');
+        $atom3 = $pb->atom('light_2');
+
+        $this->assertSame($atom, $atom2);
+        $this->assertNotSame($atom2, $atom3);
+    }
+
+    public function testExtract()
+    {
+        $pb = new \Fieg\PC\PropositionBuilder();
+
+        $pb->atom('light_1');
+        $pb->atom('light_1');
+        $pb->atom('light_2');
+
+        $this->assertFalse(isset($light_1));
+
+        extract($pb->getAtoms());
+
+        $this->assertInstanceOf('Fieg\PC\Proposition\Atomic', $light_1);
+        $this->assertFalse(isset($light_0));
+    }
+}
diff --git a/tests/bootstrap.php b/tests/bootstrap.php
new file mode 100644
index 0000000..9a6e7af
--- /dev/null
+++ b/tests/bootstrap.php
@@ -0,0 +1,3 @@
+<?php
+
+$loader = require __DIR__ . '/../vendor/autoload.php';