Proof Search Strategies in Linear Logic

Tanel Tammet

In this paper we will concentrate on problems of automated theorem proving in full propositional first-order linear logic. We will investigate general search strategies and ways for modifying standard deduction rules in linear logic to make it more suitable for automated proof search, both for "top-down" and "bottom-up" directions. The presented modifications are motivated by experiments performed with our theorem prover. We will describe the implementations and performed experiments for both search directions.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.