Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski, Uni Bremen 2008
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

Propositional.ProveWithTruthTable

Description

A truth table prover for propositional logic. Inefficient, but useful for learning purposes.

Synopsis

Documentation

ttProver :: Prover Sign FORMULA Morphism PropSL ProofTree

The Prover implementation.

Implemented are: a prover GUI.

ttConsistencyChecker :: ConsChecker Sign FORMULA PropSL Morphism ProofTree

The Consistency Cheker.

ttConservativityChecker

Arguments

:: (Sign, [Named FORMULA])

Initial sign and formulas

-> Morphism

morhpism between specs

-> [Named FORMULA]

Formulas of extended spec

-> IO (Result (Conservativity, [FORMULA])) 

Conservativity check

Conservativity Check via truth table

allModels :: Sign -> [Model]

generate all models for a signature