A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules

We devise a calculus based on the resolution and paramodulation rules and operating on schemata of formulæ. These schemata are defined inductively, using convergent rewrite systems encoding primitive recursive definitions. The main original feature of this calculus is that the rules operate on formu...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logic and computation 2017-03, Vol.27 (2), p.549-576
Main Author: Peltier, N.
Format: Article
Language:English
Subjects:
Computer Science
Logic in Computer Science
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We devise a calculus based on the resolution and paramodulation rules and operating on schemata of formulæ. These schemata are defined inductively, using convergent rewrite systems encoding primitive recursive definitions. The main original feature of this calculus is that the rules operate on formulæ or terms occurring at arbitrarily deep positions inside the considered schemata, possibly by applying transformations on the corresponding rewrite system. Each inference step in the new calculus corresponds to several applications of the usual resolution or paramodulation rules over the instances of the considered schemata. The calculus has been implemented in the proof editor Shred. As an example of application we provide a formal refutation of a schema of clause sets generated by applying the CERES cut-elimination method on Fürstenberg's proof of the infinity of prime numbers.
ISSN:0955-792X
1465-363X
DOI:10.1093/logcom/exu078