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

DOI10.1093/LOGCOM/EXU078zbMath1361.68191OpenAlexW4298955360MaRDI QIDQ2987065

Nicolas Peltier

Publication date: 17 May 2017

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exu078

zbMATH Keywords

schemasinductionresolutioninteractive theorem provingparamodulation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• Unnamed Item
• Prover9
• Mace4
• CERES
• Shred

This page was built for publication: A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules