stp (empty) → 0.1.0.0

raw patch · 7 files changed

+179/−0 lines, 7 filesdep +basedep +containersdep +regex-compatsetup-changed

Dependencies added: base, containers, regex-compat, stp

Files

• CHANGELOG.md +4/−0
• LICENSE +30/−0
• README.md +17/−0
• Setup.hs +2/−0
• example/MU.hs +21/−0
• src/SimpleTheoremProver.hs +60/−0
• stp.cabal +45/−0

@@ -0,0 +1,4 @@+# Revision history for stp++## 0.1.0.0 -- 2018-11-20+* First version.

@@ -0,0 +1,30 @@+Copyright (c) 2018, Boro Sitnikovski++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Boro Sitnikovski nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,17 @@+# Simple Theorem Prover++Simple Theorem Prover is a proof tree generator. It allows for specifying axioms and inference rules, and then by quering the program it will produce all valid combinations of inference in attempt to reach a target result.++This project is based on [Simple theorem prover in Racket](https://bor0.wordpress.com/2018/08/07/simple-theorem-prover-in-racket/).++## Prerequisites++Make sure you have `ghc` and `cabal` installed. Also, make sure that `cabal update` is ran to ensure latest version of packages is used.++## Installation++1. Run `cabal sandbox init`+1. Run `cabal install` to install dependencies and build this project+1. Run `cabal run` to run the example++Copyright 2018, Boro Sitnikovski. All rights reserved.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,21 @@+module Main where++import SimpleTheoremProver++import Text.Regex (subRegex, matchRegex, mkRegex)+import Data.List (isSuffixOf)++muRules :: [Rule String]+muRules = [+    Rule   "One"   (\thm -> if (isSuffixOf "I" thm) then (thm ++ "U") else thm)+    , Rule "Two"   (\thm -> case (matchRegex (mkRegex "M(.*)") thm) of+                                Just [x] -> thm ++ x+                                _        -> thm)+    , Rule "Three" (\thm -> subRegex (mkRegex "III") thm "U")+    , Rule "Four"  (\thm -> subRegex (mkRegex "UU") thm "")+    ]++testProver = TheoremProver (map mkAxiom ["MI"]) muRules++main :: IO ()+main = print $ findProof testProver "MIUIU" 5

@@ -0,0 +1,60 @@+module SimpleTheoremProver where++import Data.List (nubBy, find)+import Data.Set (fromList, union)++-- | Based on https://bor0.wordpress.com/2018/08/07/simple-theorem-prover-in-racket/.++-- | A rule is a way to change a theorem.+data Rule a = Rule { name :: String , function :: a -> a }++instance Show (Rule a) where+    show (Rule a _) = a++-- | A theorem is consisted of an initial axiom and rules (ordered set) applied+data Theorem a = Theorem { axiom :: a , rulesThm :: [Rule a] , result :: a } deriving (Show)++-- | A prover system is consisted of a bunch of axioms and rules to apply between them+data TheoremProver a = TheoremProver { axioms :: [Theorem a] , rulesThmProver :: [Rule a] } deriving (Show)++-- | An axiom is just a theorem already proven+mkAxiom :: a -> Theorem a+mkAxiom a = Theorem a [] a++-- | Applies a single rule to a theorem+thmApplyRule :: Theorem a -> Rule a -> Theorem a+thmApplyRule theorem rule =+    Theorem+    (axiom theorem)+    (rulesThm theorem ++ [rule])+    ((function rule) (result theorem))++-- | Applies all prover's rules to a list of theorems+thmApplyRules :: TheoremProver a -> [Theorem a] -> [Theorem a]+thmApplyRules prover (thm:thms) = map (thmApplyRule thm) (rulesThmProver prover) ++ (thmApplyRules prover thms)+thmApplyRules _ _ = []++-- | Merge two list of proofs but skip duplicate proofs, giving the first argument priority+-- This is used to avoid circular results in the search tree+-- E.g. application of rules resulting in an earlier theorem/axiom+mergeProofs :: Eq a => [Theorem a] -> [Theorem a] -> [Theorem a]+mergeProofs p1 p2 = nubBy (\t1 t2 -> result t1 == result t2) p1 ++ p2++-- | Finds a proof by constructing a proof tree by iteratively applying theorem rules+findProofIter :: (Ord a, Eq a) => TheoremProver a -> a -> Int -> [Theorem a] -> Maybe (Theorem a)+findProofIter _ _ 0 _ = Nothing+findProofIter prover target depth foundProofs = case (find (\x -> target == result x) foundProofs) of+    Just prf -> Just prf+    Nothing  -> +        let theorems = thmApplyRules prover foundProofs+            proofsSet = fromList (map result foundProofs)+            theoremsSet = fromList (map result theorems) in+        if (union proofsSet theoremsSet) == proofsSet+        -- The case where no new theorems were produced, that is, A union B = A+        then Nothing+        -- Otherwise keep producing new proofs+        else findProofIter prover target (depth - 1) (mergeProofs foundProofs theorems)++-- | Find proof helper+findProof :: Ord a => TheoremProver a -> a -> Int -> Maybe (Theorem a)+findProof prover target depth = findProofIter prover target depth (axioms prover)

@@ -0,0 +1,45 @@+name:                stp+version:             0.1.0.0+synopsis:            Simple Theorem Prover+copyright:           (c) 2018 Boro Sitnikovski+homepage:            https://github.com/bor0/stp+license:             BSD3+license-file:        LICENSE+author:              Boro Sitnikovski+maintainer:          buritomath@gmail.com+category:            Math+build-type:          Simple+extra-source-files:  CHANGELOG.md+cabal-version:       >=1.10+description:+    Simple Theorem Prover constructs a proof tree+    and searches for a target/conclusion given a+    list of rewrite rules and axioms/theorems.+extra-source-files:+    CHANGELOG.md+    README.md+    LICENSE++source-repository head+    type: git+    location: https://github.com/bor0/stp++source-repository this+    type: git+    tag: 0.1.0.0+    location: https://github.com/bor0/stp++library+    exposed-modules:     SimpleTheoremProver+    build-depends:       base >=4.11 && <4.12+                         , containers ==0.5.11.0+    hs-source-dirs:      src+    default-language:    Haskell2010++executable mu-test+    main-is:             MU.hs+    build-depends:       base >=4.11 && <4.12+                         , regex-compat ==0.95.1+                         , stp+    hs-source-dirs:      example+    default-language:    Haskell2010