diff options
| author | aarne <aarne@cs.chalmers.se> | 2005-12-20 14:20:42 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2005-12-20 14:20:42 +0000 |
| commit | 25b31684378d3b0668b65939fc7b30b0c1e8d130 (patch) | |
| tree | 7ed3e007a8847096087a3593504aec526fedd455 /examples/systemS/ex2.txt | |
| parent | 774abf612d5cc3a099f229c9cc649c7c51979f2d (diff) | |
CS's system S
Diffstat (limited to 'examples/systemS/ex2.txt')
| -rw-r--r-- | examples/systemS/ex2.txt | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/examples/systemS/ex2.txt b/examples/systemS/ex2.txt new file mode 100644 index 000000000..1dffb6bf9 --- /dev/null +++ b/examples/systemS/ex2.txt @@ -0,0 +1,13 @@ +[ A -> B |- ~ B -> ~ A ] +------------------------------ Implication strategy +[ A -> B , ~ B |- ~ A ] +------------------------------ Negation rewrite +[ A -> B , ~ B |- A -> _|_ ] +------------------------------ Implication strategy +[ A , A -> B , ~ B |- _|_ ] +------------------------------ Modus ponens +[ A , A -> B , B , ~ B |- _|_ ] +------------------------------ Forgetting +[ B , ~ B |- _|_ ] +------------------------------ Ex falso quodlibet _|_ +Ø |