Connection-Based Theorem Proving in Classical and Non-Classical Logics

摘要

We present a uniform procedure for proof search in classical logic, intuitionistic logic, various modal logics, and fragments of linear logic. It is based on matrix characterizations of validity in these logics and extends Bibel's connection method, origi