Computational logic based on linear logic and fixed points

We use µMALL, the logic that results from adding least and greatest fixed points to first-order multiplicative-additive linear logic, as a framework for presenting several topics in computational logic. In particular, we present various levels of restrictions on the roles of fixed points in proofs and show that these levels capture different topics. For example, level 0 of µMALL captures (generalized) unification problems, level 1 captures Horn-clause logic programming, level 2 captures various model checking problems, and level 3 introduces a linearized form of arithmetic. We also show how the proof search interpretation of µMALL can be used to compute general recursive functions. Finally, we identify several situations where provability in Peano Arithmetic can be replaced by provability in µMALL. In such situations, the proof theory of µMALL can be used to study and implement proof search procedures for fragments of Peano Arithmetic