LicenseGNU LGPLv3
Maintainerpaul.bittner@uni-ulm.de
Safe HaskellSafe

Logic

Description

Type class for reasoning on Logics.

Synopsis

Documentation

class Logic l where Source #

Type class to reason on logics. We use this type class to reason on propositional logic and the ternary logic by Sobocinski we use for feature trace recording.

Minimal complete definition

ltrue, lfalse, lnot, land, leval

Methods

ltrue :: l Source #

The atomic value representing true in this logic.

lfalse :: l Source #

The atomic value representing false in this logic.

lvalues :: [l] Source #

A list of all atomic values of this logic. Default implementation comprises ltrue and lfalse.

lnot :: l -> l Source #

Negation of a logical formula.

land :: [l] -> l Source #

Conjunction of a list of logical formulas.

lor :: [l] -> l Source #

Disjunction of a list of logical formulas.

limplies :: l -> l -> l Source #

Implication between two logical formulas. The first argument p is one the left side of the implication and the second argument q is on the right (i.e., p => q).

lequals :: l -> l -> l Source #

Equivalence between two logical formulas.

leval :: (l -> l) -> l -> l Source #

Evaluates a logical formula. Arguments are

  1. a function assigning variables to values
  2. a formula to evaluate This function should return an element of lvalues.

Instances

Instances details
Logic a => Logic (Maybe a) Source #

Any Logic can be lifted to a logic on Maybe. This adds a new value Nothing to the values of the given logic. In particular, NullableFormula is thus a Logic.

Instance details

Defined in NullPropositions

Methods

ltrue :: Maybe a Source #

lfalse :: Maybe a Source #

lvalues :: [Maybe a] Source #

lnot :: Maybe a -> Maybe a Source #

land :: [Maybe a] -> Maybe a Source #

lor :: [Maybe a] -> Maybe a Source #

limplies :: Maybe a -> Maybe a -> Maybe a Source #

lequals :: Maybe a -> Maybe a -> Maybe a Source #

leval :: (Maybe a -> Maybe a) -> Maybe a -> Maybe a Source #

Logic (PropositionalFormula a) Source #

PropositionalFormulas form a Logic.

Instance details

Defined in Propositions