| Copyright | (c) Artem Mavrin 2021 |
|---|---|
| License | BSD3 |
| Maintainer | artemvmavrin@gmail.com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | Safe |
| Language | Haskell2010 |
AutoProof.Internal.Formula.Operations
Description
Defines miscellaneous operations on formulas.
Synopsis
- subformulas :: Ord a => Formula a -> Set (Formula a)
- substitute :: Eq a => Formula a -> a -> Formula a -> Formula a
- getAnyVariable :: Formula a -> Maybe a
Documentation
subformulas :: Ord a => Formula a -> Set (Formula a) Source #
Get the set of subformulas of a propositional formula.
Examples
>>>subformulas $ Or (Var 'x') (And (Var 'y') (Var 'z'))fromList [Var 'x',Var 'y',Var 'z',And (Var 'y') (Var 'z'),Or (Var 'x') (And (Var 'y') (Var 'z'))]
substitute :: Eq a => Formula a -> a -> Formula a -> Formula a Source #
( represents \(a[p/x]\), the substitution of each
occurence of the variable \(x\) in the formula \(a\) by the formula \(p\).substitute a x p)
Examples
>>>substitute (Imp (Var 'e') (Var 'e')) 'e' (And (Var 'a') (Var 'a'))Imp (And (Var 'a') (Var 'a')) (And (Var 'a') (Var 'a'))
getAnyVariable :: Formula a -> Maybe a Source #
Obtain a propositional variable from a formula, if there is one.
Examples
>>>getAnyVariable (Or (Var "a") (Var "b"))Just "a"
>>>getAnyVariable (Lit False :: Formula String)Nothing