Lambda P-: A Pure Type System for First Order Logic with Automated Theorem211 Proving

摘要

In this document, we define multi sorted first order logic and discuss several211u001eproof systems for this logic: natural deduction, tableau methods, resolution 211u001emethods and the framework of Pure Type Systems.