KnowledgeBase » 
PUBLICATION
» ID = 744
Intuitionistic Ancestral Logic
by Liron Cohen, Robert L. Constable
2015
- Published in the Journal of Logic and Computation: exv073v1-exv073, Oct 10, 2015.
- Official PDF
In this paper we define pure intuitionistic Ancestral Logic (iAL), extending pure intuitionistic First-Order Logic (iFOL). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL given by its realizer for the transitive closure, TC. We derive this operator from the natural type theoretic definition of TC using intersection. We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further show that iAL subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes. We also extract schemes from proofs that iAL specifications are solvable.