autoproof-0.0.0.0: Propositional logic library
Copyright(c) Artem Mavrin 2021
LicenseBSD3
Maintainerartemvmavrin@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe
LanguageHaskell2010

AutoProof.Internal.Proof.Structural

Description

Structural rules to transform proofs.

Synopsis

Documentation

weakenProof :: Ord a => Proof a -> Formula a -> Proof a Source #

The weakening structural rule. (weakenProof p a) modifies the proof p to include a as an additional hypothesis.

strengthenProof :: Ord a => Proof a -> Proof a Source #

Strengthen a proof by preserving its structure but removing redundant hypotheses where possible.