The CoRe calculus

Abstract

We present the CoRE calculus for contextual reasoning which supports reasoning directly at the assertion level, where proof steps are justified in terms of applications of definitions, lemmas, theorems, or hypotheses (collectively called "assertions") and which is an established basis to generate proof presentations in natural language. The calculus comprises a uniform notion of a logical context of subformulas as well as replacement rules available in a logical context. Replacement rules operationalize assertion level proof steps and technically are generalized resolution and paramodulation rules, which in turn should suit the implementation of automatic reasoning procedures. © Springer-Verlag Berlin Heidelberg 2005.