picologic alternatives and similar packages
Based on the "Logic" category.
Alternatively, view picologic alternatives based on common mentions on social networks and blogs.

tamarinprover
Main source code repository of the Tamarin prover for security protocol verification. 
atphaskell
Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning" 
logicclasses
Framework for propositional and first order logic, theorem proving 
obdd
pure Haskell implementation of reduced ordered binary decision diagrams 
structuralinduction
SII: Structural Induction Instantiator over any strictlypositive algebraic data type. 
g4ipprover
Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip 
tpdb
parser and prettyprinter for TPDB syntax (termination problem data base) 
haskholcore
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
Static code analysis for 29 languages.
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of picologic or a related project?
README
Picologic
Picologic is a lightweight library for working with symbolic logic expressions. It is built against the picosat Haskell library which bundles the SAT solver with the Haskell package so no external solver or dependencies are necessary.
Picologic provides the logic expressions, parser and normal form conversion, and Tseytin transformations to express the logic expressions in equational form and generate constraint sets for use in SAT/SMT solvers.
Installing
To use the library using Stack use:
$ git clone [email protected]:sdiehl/picologic.git
$ cd picologic
$ stack build
$ stack test
Or using Cabal:
$ cabal install picologic
To build the interactive shell compile with the fshell
flag:
$ cabal get picologic
$ cd picologic0.2.0
$ cabal configure fshell
$ cabal install
Usage
To use the API import the Picologic
module.
import Picologic
p, q, r :: Expr
p = readExpr "~(A  B)"
q = readExpr "(A  ~B  C) & (B  D  E) & (D  F)"
r = readExpr "(φ <> ψ)"
s = readExpr "(0  A) > (A & 1)"
ps = ppExprU p
 ¬(A ∨ B)
qs = ppExprU q
 ((((A ∨ ¬B) ∨ C) ∧ ((B ∨ D) ∨ E)) ∧ (D ∨ F))
rs = ppExprU (cnf r)
 ((φ ∧ (φ ∨ ¬ψ)) ∧ ((ψ ∨ ¬φ) ∧ ψ))
ss = ppExprU s
 ((⊥ ∨ A) → (A ∧ ⊤))
ss1 = ppExprU (cnf s)
 ⊤
main :: IO ()
main = solveProp p >>= putStrLn . ppSolutions
 ¬A ¬B
 ¬A B
 A ¬B
The expression AST consists just of the logical connectives or constants.
newtype Ident = Ident String
deriving (Eq, Ord, Show, Data, Typeable)
data Expr
= Var Ident  ^ Variable
 Neg Expr  ^ Logical negation
 Conj Expr Expr  ^ Logical conjunction
 Disj Expr Expr  ^ Logical disjunction
 Iff Expr Expr  ^ Logical biconditional
 Implies Expr Expr  ^ Material implication
 Top  ^ Constant true
 Bottom  ^ Constant false
deriving (Eq, Ord, Show, Data, Typeable)
To use the interactive shell when compiled with with fshell
invoke
picologic
at the shell.
$ picologic
Picologic 0.1
Type :help for help
Logic> p  q
(p ∨ q)
Solutions:
p q
¬p q
p ¬q
Logic> ~(a > (b <> c))
(a ∧ ((b ∨ c) ∧ (¬b ∨ ¬c)))
Solutions:
¬a ¬b c
a b ¬c
¬a b ¬c
a ¬b c
Logic> :clauses
[[2,3],[2,3],[2,3,2,3],[1,2,3,2,3]]
License
Released under the MIT License. Copyright (c) 20142020, Stephen Diehl
*Note that all licence references and agreements mentioned in the picologic README section above
are relevant to that project's source code only.