HomeIsabelle/Phabricator
Diffusion afp-devel ac00f34583b0

new entry Saturation_Framework_Extensions
ac00f34583b0
Actions

Description

new entry Saturation_Framework_Extensions

Details

Provenance
paulson <lp15@cam.ac.uk>Authored on
Parents
rAFPa41d53bc4c69: a proof of concept for generic conversions
Branches
Unknown
Tags
Unknown

Changes (12)

PathSize

rAFPac00f34583b0

View Options

thys/ROOTS

Loading...
View Options

thys/Saturation_Framework_Extensions/Clausal_Calculus.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/Consistency_Preservation.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/Given_Clause_Architectures_Revisited.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/ROOT

Loading...
View Options

thys/Saturation_Framework_Extensions/Soundness.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/document/root.tex

Loading...