Editing Computability logic (section)

==As a problem solving tool== 
The known deductive systems for various fragments of CoL share the property that a solution (algorithm) can be automatically extracted from a proof of a problem in the system. This property is further inherited by all applied theories based on those systems.  So, in order to find a solution for a given problem, it is sufficient to express it in the language of CoL and then find a proof of that expression. Another way to look at this phenomenon is to think of a formula ''G'' of CoL as [[program specification]] (goal). Then a proof of ''G'' is – more precisely, translates into – a program meeting that specification. There is no need to verify that the specification is met, because the proof itself is, in fact, such a verification. 

Examples of CoL-based applied theories are the so-called ''clarithmetics''. These are number theories based on CoL in the same sense as [[Peano_axioms#Peano_arithmetic_as_first-order_theory|first-order Peano arithmetic]] PA is based on classical logic. Such a system is usually a conservative extension of PA. It typically includes all Peano axioms, and adds to them one or two extra-Peano axioms such as <big><big>⊓</big></big>''x''<big><big>⊔</big></big>''y''(''y''=''x''') expressing the computability of the successor function. Typically it also has one or two non-logical rules of inference, such as constructive versions of [[mathematical induction|induction]] or [[comprehension axiom|comprehension]]. Through routine variations in such rules one can obtain [[soundness (logic)|sound]] and [[completeness (logic)|complete]] systems characterizing one or another interactive computational complexity class ''C''. This is in the sense that a problem belongs to ''C'' if and only if it has a proof in the theory. So, such a theory can be used for finding not merely algorithmic solutions, but also efficient ones on demand, such as solutions that run in [[polynomial time]] or [[logarithmic space]]. It should be pointed out that all clarithmetical theories share the same logical postulates, and only their non-logical postulates vary depending on the target complexity class. Their notable distinguishing feature from other approaches with similar aspirations (such as [[bounded arithmetic]]) is that they extend rather than weaken PA, preserving the full deductive power and convenience of the latter.