From 46347da5454f2a10dd1ca167d14eb4dda91bad18 Mon Sep 17 00:00:00 2001 From: fieg Date: Tue, 3 Jun 2014 00:20:53 +0200 Subject: [PATCH] Initial commit --- .gitignore | 1 + .scrutinizer.yml | 57 ++ .travis.yml | 27 + README.md | 6 + composer.json | 25 + composer.lock | 720 ++++++++++++++++++ phpunit.xml.dist | 27 + src/Fieg/PC/CompoundProposition.php | 43 ++ src/Fieg/PC/KnowledgeBase.php | 135 ++++ .../PC/Proof/DeductionBottomUpStrategy.php | 89 +++ src/Fieg/PC/Proof/ProofStrategyInterface.php | 13 + src/Fieg/PC/Proposition.php | 12 + src/Fieg/PC/Proposition/AndX.php | 36 + src/Fieg/PC/Proposition/Atomic.php | 33 + src/Fieg/PC/Proposition/Implies.php | 52 ++ src/Fieg/PC/Proposition/NotX.php | 30 + src/Fieg/PC/Proposition/OrX.php | 22 + src/Fieg/PC/PropositionBuilder.php | 93 +++ tests/Fieg/PC/KnowledgeBaseTest.php | 155 ++++ tests/Fieg/PC/PropositionBuilderTest.php | 51 ++ tests/bootstrap.php | 3 + 21 files changed, 1630 insertions(+) create mode 100644 .gitignore create mode 100644 .scrutinizer.yml create mode 100644 .travis.yml create mode 100644 README.md create mode 100644 composer.json create mode 100644 composer.lock create mode 100644 phpunit.xml.dist create mode 100644 src/Fieg/PC/CompoundProposition.php create mode 100644 src/Fieg/PC/KnowledgeBase.php create mode 100644 src/Fieg/PC/Proof/DeductionBottomUpStrategy.php create mode 100644 src/Fieg/PC/Proof/ProofStrategyInterface.php create mode 100644 src/Fieg/PC/Proposition.php create mode 100644 src/Fieg/PC/Proposition/AndX.php create mode 100644 src/Fieg/PC/Proposition/Atomic.php create mode 100644 src/Fieg/PC/Proposition/Implies.php create mode 100644 src/Fieg/PC/Proposition/NotX.php create mode 100644 src/Fieg/PC/Proposition/OrX.php create mode 100644 src/Fieg/PC/PropositionBuilder.php create mode 100644 tests/Fieg/PC/KnowledgeBaseTest.php create mode 100644 tests/Fieg/PC/PropositionBuilderTest.php create mode 100644 tests/bootstrap.php 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 @@ + + + + + + + + tests + + + + + + src/ + + + 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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ + + * @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 @@ +