Implementing program extraction from CL1-proofs

Abstract

Computability logic (CoL) is a formal theory of interactive computation. It understands computational problems as games played by two players: a machine and its environment, uses logical formalism to describe valid principles of computability and formulas to represent computational problems. Logic CL1 is a deductive system for a fragment of CoL. The logical vocabulary contains all of the operators of classical logic and choice operators, the atoms represent elementary games i.e. predicates of classical logic. In this paper, we present a program that takes a CL1-proof of an arbitrary formula $F$, and extract a winning strategy for $F$ from that proof then play $F$ using that strategy. We hope this paper would provide a starting point for further work in program extraction of the CoL-based arithmetic and other CoL-based applied systems.

1 figure

References in corpus (13)

• Sequential operators in computability logic
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Propositional computability logic I
• Cirquent calculus deepened
• Computability Logic: a formal theory of interaction
• From truth to computability I
• The intuitionistic fragment of computability logic at the propositional level
• Intuitionistic computability logic
• Many concepts and two logics of algorithmic reduction
• The taming of recurrences in computability logic through cirquent calculus, Part I
• Toggling operators in computability logic
• The parallel versus branching recurrences in computability logic
• On the system CL12 of computability logic