Proof Search Strategies in Linear Logic

Contents

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.