3 ms·
Theorem proving in intuitionistic logic is a two-player game and maps perfectly to the kind of Monte-Carlo Tree Search that's employed here. Except that it is f
by fmap 9y ago
Theorem proving in intuitionistic logic is a two-player game and maps perfectly to the kind of Monte-Carlo Tree Search that's employed here. Except that it is far more difficult than Chess/Go/etc., since the branching factor is essentially unbounded.
- seanwilson 9y agoCan you elaborate? How could you score how close you are to a solution and what would the second player be doing?
- fmap 9y agoConsider a formula made up of only conjunctions and disjunctions and true/false. The first player tries to prove the formula and gets to move at every disjunction and is allowed to select which side of the disjunction to prove. The second player tries to prevent the first player from finding a proof and gets to move at every conjunction, selecting a side of the conjunction to descend to. The final state here is an atomic proposition which is either true or false and determines which player won. You derive a value function from that in the same way as you do for Go or Chess. You can extend this idea to full first-order intuitionistic logic and probably also to higher-order logics, as well as many different modal logics. There are also formulations of classical logic as a single player game, but that doesn't seem to be very useful here.