picologic alternatives and similar packages
Based on the "Logic" category.
Alternatively, view picologic alternatives based on common mentions on social networks and blogs.
tamarin-prover9.8 0.0 picologic VS tamarin-proverMain source code repository of the Tamarin prover for security protocol verification.
smcdel7.9 0.0 picologic VS smcdelA symbolic model checker for Dynamic Epistemic Logic.
hatt7.7 0.0 picologic VS hattTruth-table generator for classical propositional logic
tip-haskell-frontendConvert from Haskell to Tip
picosat6.9 0.0 L2 picologic VS picosatHaskell bindings for PicoSAT solver
atp-haskell6.6 0.0 picologic VS atp-haskellHaskell version of the code from "Handbook of Practical Logic and Automated Reasoning"
jukebox6.5 0.0 picologic VS jukeboxA theorem prover
hout6.3 0.0 picologic VS houtA non-interactive proof assistant using the Haskell type system
Heyting Algebras5.8 0.0 picologic VS Heyting AlgebrasHeyting Algebras in Haskell
logic-classes5.7 0.0 picologic VS logic-classesFramework for propositional and first order logic, theorem proving
Folly5.6 0.0 picologic VS FollyFirst order logic in Haskell
obdd5.4 0.0 picologic VS obddpure Haskell implementation of reduced ordered binary decision diagrams
structural-inductionSII: Structural Induction Instantiator over any strictly-positive algebraic data type.
qed3.9 0.0 picologic VS qedExperiments writing a prover
g4ip-prover3.4 0.0 picologic VS g4ip-proverTheorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip
tpdb3.0 0.0 picologic VS tpdbparser and prettyprinter for TPDB syntax (termination problem data base)
satchmo3.0 0.0 picologic VS satchmoSAT encoder
g4ip2.1 0.0 picologic VS g4ipA theorem prover using G4ip
minisat2.1 0.0 picologic VS minisatMinisat Haskell bundle
judge1.5 0.0 picologic VS judgeTableau-based theorem prover for justification logic.
haskhol-core0.8 0.0 picologic VS haskhol-coreThe core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
Access the most powerful time series database as a service
* 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?
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.
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
$ cabal get picologic $ cd picologic-0.2.0 $ cabal configure -fshell $ cabal install
To use the API import the
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
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]]
Released under the MIT License. Copyright (c) 2014-2020, 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.