hatt alternatives and similar packages
Based on the "Logic" category.
Alternatively, view hatt 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 
structuralinduction
SII: Structural Induction Instantiator over any strictlypositive algebraic data type. 
g4ipprover
Theorem prover for intuitionistic propositional logic, fork of github.com/cacay/G4ip 
haskholcore
The core logical system of the HaskHOL theorem prover. See haskhol.org for more details.
* 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 hatt or a related project?
Popular Comparisons
README
Hatt
Hatt is a commandline program which prints truth tables for expressions in classical propositional logic, and a library allowing its parser, evaluator, truth table generator and other functionality to be used in other programs.
Installation
Hatt is available from Hackage. To install it with cabalinstall
, update
your list of known packages and then install Hatt.
$ cabal update
$ cabal install hatt
To build it from source, cd
into the directory containing the Hatt source
files, including hatt.cabal
, and run cabal install
.
Valid Hatt expressions
The following are all valid expression forms which can be parsed by Hatt, where
ϕ
and ψ
are metalinguistic variables standing in for any valid expression.
Hatt accepts the standard Unicode symbols for logical connectives. This is
useful when pasting example formulae from the web or using Hatt in pretty
mode.
 Variables:
P
,Q
,a
,b
etc.basically anything in the character class[azAZ]
 Negation:
~ϕ
or¬ϕ
 Conjunction:
(ϕ & ψ)
or(ϕ ∧ ψ)
 Disjunction:
(ϕ  ψ)
or(ϕ ∨ ψ)
 Conditional:
(ϕ > ψ)
or(ϕ → ψ)
 Biconditional:
(ϕ <> ψ)
or(ϕ ↔ ψ)
Parentheses are not required around toplevel formulae, regardless of whether
the primary connective is binary. For example, the expression a  b
is valid
and will be parsed correctly, as would p <> (q & ~r)
, although the
parenthesised versions of both these expressions ((a  b)
and
(p <> (q & ~r))
) are also fine.
Standard operator precedence for logical operators is supported. All the
binary connectives associate to the right, so a > b > c
is interpreted as
a > (b > c)
. To override these rules, use parentheses as normal. Note that
rightassociativity only matters for the material conditional: all the other
logical operators are associative, so a * (b * c)
is equivalent to
(a * b) * c
where *
is conjunction, disjunction or the biconditional.
Using the hatt
commandline program
The default mode is interactive: you start the program, enter expressions at the prompt, and their truth tables are printed. Here's an example session.
$ hatt
Entering interactive mode. Type `help` if you don't know what to do!
> A  B
A B  (A  B)

T T  T
T F  T
F T  T
F F  F
> p > (q & ~r)
p q r  (p > (q & ~r))

T T T  F
T T F  T
T F T  F
T F F  F
F T T  T
F T F  T
F F T  T
F F F  T
> e <> f
e f  (e <> f)

T T  T
T F  F
F T  F
F F  T
> exit
The evaluate
flag lets you pass a single expression to be evaluated
directly.
$ hatt evaluate="P > (Q  ~R)"
P Q R  (P > (Q  ~R))

T T T  F
T T F  F
T F T  F
T F F  F
F T T  F
F T F  F
F F T  T
F F F  F
By default, hatt
will print ASCII representations of expressions. If you have
a Unicodecapable terminal, try passing the pretty
option to prettyprint
expressions using the more common logical symbols.
$ hatt evaluate="P > (Q  ~R)" pretty
P Q R  (P → (Q ∨ ¬R))

T T T  F
T T F  F
T F T  F
T F F  F
F T T  F
F T F  F
F F T  T
F F F  F
You can enable prettyprinting while in interactive mode by using the pretty
command.
If you pass the coloured
flag, hatt
will colour the truth values in the
tables which it prints: green for true, red for false. You can enable colouring
during interactive mode by using the colour
command.
You can print out the normal forms of expressions too, by prefixing an
expression with nnf
, dnf
or cnf
.
$ hatt pretty
> nnf ~(P > (Q & R))
(P ∧ (¬Q ∨ ¬R))
The three supported normal forms are negation normal form, conjunctive normal form and disjunctive normal form.
Using Hatt in other programs
Hatt exposes the Data.Logic.Propositional
module, which provides a simple API
for parsing, evaluating, and printing truth tables. It also includes the
Data.Logic.Propositional.NormalForms
module which exports functions to convert
logical expressions into normal forms. Details of the foregoing can be found in
the library documentation.