Relaxed weighted path order in theorem proving

DOI10.1007/s11786-020-00474-0zbMath1488.68139OpenAlexW3014201085WikidataQ108482108 ScholiaQ108482108MaRDI QIDQ2209265

Jan Jakubův, Cezary Kaliszyk

Publication date: 30 October 2020

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-020-00474-0

zbMATH Keywords

first-order logicterm rewritingautomated theorem provingsuperposition calculusterm orderingsweighted path order

Mathematics Subject Classification ID

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

Uses Software

• VAMPIRE
• TPTP
• E Theorem Prover
• BliStrTune
• CoqHammer

Cites Work

• Things to know when implementing KBO
• Solution of the Robbins problem
• Towards a unified ordering for superposition-based automated reasoning
• Hammer for Coq: automation for dependent type theory
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• System Description: E 1.8
• The 8th IJCAR automated theorem proving system competition – CASC-J8
• AC-KBO revisited
• Hierarchical invention of theorem proving strategies