| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Logic.ATP.FOL
Description
Basic stuff for first order logic.
Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
Synopsis
- class (IsQuantified formula, HasApply (AtomOf formula), IsTerm (TermOf (AtomOf formula)), VarOf formula ~ TVarOf (TermOf (AtomOf formula))) => IsFirstOrder formula
- data Interp function predicate d
- holds :: FiniteInterpretation a function predicate v dom => Interp function predicate dom -> Map v dom -> a -> Bool
- holdsQuantified :: forall formula function predicate dom. (IsQuantified formula, FiniteInterpretation (AtomOf formula) function predicate (VarOf formula) dom, FiniteInterpretation formula function predicate (VarOf formula) dom) => Interp function predicate dom -> Map (VarOf formula) dom -> formula -> Bool
- holdsAtom :: (HasEquate atom, IsTerm term, Eq dom, term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) => Interp function predicate dom -> Map v dom -> atom -> Bool
- termval :: (IsTerm term, v ~ TVarOf term, function ~ FunOf term) => Interp function predicate r -> Map v r -> term -> r
- var :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => formula -> Set v
- fv :: (IsFirstOrder formula, v ~ VarOf formula) => formula -> Set v
- fva :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => atom -> Set v
- fvt :: (IsTerm term, v ~ TVarOf term) => term -> Set v
- generalize :: IsFirstOrder formula => formula -> formula
- subst :: (IsFirstOrder formula, term ~ TermOf (AtomOf formula), v ~ VarOf formula) => Map v term -> formula -> formula
- substq :: (IsFirstOrder formula, v ~ VarOf formula, term ~ TermOf (AtomOf formula)) => Map v term -> (v -> formula -> formula) -> v -> formula -> formula
- asubst :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> atom -> atom
- tsubst :: (IsTerm term, v ~ TVarOf term) => Map v term -> term -> term
- lsubst :: (JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> lit -> lit
- bool_interp :: Interp FName Predicate Bool
- mod_interp :: Int -> Interp FName Predicate Int
- type ApFormula = QFormula V ApAtom
- type EqFormula = QFormula V EqAtom
- testFOL :: Test
Documentation
class (IsQuantified formula, HasApply (AtomOf formula), IsTerm (TermOf (AtomOf formula)), VarOf formula ~ TVarOf (TermOf (AtomOf formula))) => IsFirstOrder formula Source #
Combine IsQuantified, HasApply, IsTerm, and make sure the term is using the same variable type as the formula.
Instances
| IsFirstOrder ApFormula Source # | |
Defined in Data.Logic.ATP.FOL | |
| IsFirstOrder EqFormula Source # | |
Defined in Data.Logic.ATP.FOL | |
| IsFirstOrder Formula Source # | |
Defined in Data.Logic.ATP.Skolem | |
Semantics
data Interp function predicate d Source #
Specify the domain of a formula interpretation, and how to interpret its functions and predicates.
holds :: FiniteInterpretation a function predicate v dom => Interp function predicate dom -> Map v dom -> a -> Bool Source #
holdsQuantified :: forall formula function predicate dom. (IsQuantified formula, FiniteInterpretation (AtomOf formula) function predicate (VarOf formula) dom, FiniteInterpretation formula function predicate (VarOf formula) dom) => Interp function predicate dom -> Map (VarOf formula) dom -> formula -> Bool Source #
Implementation of holds for IsQuantified formulas.
holdsAtom :: (HasEquate atom, IsTerm term, Eq dom, term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) => Interp function predicate dom -> Map v dom -> atom -> Bool Source #
Implementation of holds for atoms with equate predicates.
termval :: (IsTerm term, v ~ TVarOf term, function ~ FunOf term) => Interp function predicate r -> Map v r -> term -> r Source #
Free Variables
var :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => formula -> Set v Source #
Find all the variables in a formula. var :: (IsFirstOrder formula, v ~ VarOf formula) => formula -> Set v
fv :: (IsFirstOrder formula, v ~ VarOf formula) => formula -> Set v Source #
Find the free variables in a formula.
fva :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => atom -> Set v Source #
Find the variables in an atom
generalize :: IsFirstOrder formula => formula -> formula Source #
Universal closure of a formula.
Substitution
subst :: (IsFirstOrder formula, term ~ TermOf (AtomOf formula), v ~ VarOf formula) => Map v term -> formula -> formula Source #
Substitution in formulas, with variable renaming.
substq :: (IsFirstOrder formula, v ~ VarOf formula, term ~ TermOf (AtomOf formula)) => Map v term -> (v -> formula -> formula) -> v -> formula -> formula Source #
Substitution within quantifiers
asubst :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> atom -> atom Source #
Substitution within atoms.
tsubst :: (IsTerm term, v ~ TVarOf term) => Map v term -> term -> term Source #
Substitution within terms.
lsubst :: (JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> lit -> lit Source #
Substitution within a Literal