Skip to content
Branch: master
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
CyclicCore.tla
FiniteSetFacts.tla
Lattices.tla
Makefile
MinCover.tla
Optimization.tla
Orthotopes.tla
README
StrongReduction.tla

README

A TLA+ specification and proofs of relevant properties for
an algorithm that computes the cyclic core of a minimal
covering problem. This algorithm was originally proposed
in the context of two-level logic minimization.

The modules:

FiniteSetTheorems,
Functions,
FunctionTheorems,
NaturalsInduction,
SequenceTheorems,
TLAPS,
WellFoundedInduction

can be found in the distribution of TLAPS v1.4.3:

http://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.3.tar.gz

The proofs have been checked with TLAPS v1.4.3, in the presence of:
    - Zenon v0.7.2
    - CVC3 v2.4.1
    - Isabelle v2011-1
    - LS4 (commit c5e907eb3be9d454b3365e747c05100bdffa939c)

This document accompanies the dissertation available at:

http://resolver.caltech.edu/CaltechTHESIS:12172017-171304566
You can’t perform that action at this time.