Logic-Independent Proof Search in Logical Frameworks (extended report)

An important question in research on logical framework is whether they can induce a logic-independent automated theorem prover. While many theorem proving innovations can indeed be generalized to large classes of logics, practically competitive provers usually require logic-specific optimizations. To investigate this question more deeply, we build a suite of modular logic definitions in a logical framework and generate Prolog-based theorem provers for them. We focus on generality and avoid taking logicspecific knowledge into account. Our generated provers support natural deduction proof search, including backchaining, as well as tableau provers and model generators. Even though these efforts have only just started, we are already able to use the latter in a system for natural language understanding that combines grammatical with semantic processing.