Schematic refutations of formula schemata

DOI10.1007/S10817-020-09583-8OpenAlexW3107513461MaRDI QIDQ2666952

Anela Lolic, David M. Cerna, Alexander Leitsch

Publication date: 23 November 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1902.08055

zbMATH Keywords

inductionresolutionschematic formulasschematic proofs

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• CERES

Cites Work

• Unnamed Item
• Methods of cut-elimination
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Cut-elimination for a logic with definitions and induction
• Schematic Cut Elimination and the Ordered Pigeonhole Principle
• A Resolution Calculus for First-order Schemata
• Decidability and Undecidability Results for Propositional Schemata
• Sequent calculi for induction and infinite descent
• Cut-Elimination and Proof Schemata
• Term Rewriting and All That
• Automated Reasoning with Analytic Tableaux and Related Methods
• Herbrand Sequent Extraction
• Resolution in type theory
• OUP accepted manuscript
• Cut-elimination and redundancy-elimination by resolution
• Proof theory

This page was built for publication: Schematic refutations of formula schemata