SCS Undergraduate Thesis Topics

Linear logic is a refinement of a mathematical logic that disallows weakening and contraction. This enables linear logic to treat propositions as resources that are part of a state and are generated and consumed, thus allowing modeling of state. Linear logic is useful in any realm that deals with reasoning about state; this includes planning problems and verification of hardware, software, and security protocols. We demonstrate various methods for improving the speed of an automated deduction system for linear logic: filtering of sequents, exploitation of a recently developed notion of left or right propositional bias, and use of a weighting heuristic for fact selection. Each of these methods reduces the number of facts and iterations required by the prover to find a proof of a given theorem. Finally, we demonstrate that the resulting reduction in facts and iterations translates into a significant clock-time speedup, improving suitability for the various applications outlined above.