ON OPTIMIZING PROOF SEARCH IN LINEAR LOGIC BY VALUE ITERATION METHOD
Valerie Novitzká, Anita Verbová · 2007
SUMMARY In this article we are interested in proving of linear logic sequents. In linear sequent calculus one sequent can have more than one proof tree. We choose the best among them satisfying some criterion. There can occur some non-deterministic choices in the process of building the proof of a sequent. We introduce probabilities to these proof constructions. Therefore we can apply one method of stochastic programming (value iteration method) to determine the optimal way in the proof search.