Relaxed weighted path order in theorem proving

DOI10.1007/S11786-020-00474-0MaRDI QIDQ2209265zbMATH OpenOpenAlexWikidataFDO

Authors Jan Jakubův, Cezary Kaliszyk

Publication date 30 October 2020

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

automated theorem provingfirst-order logicsuperposition calculusterm orderingsterm rewritingweighted path order

Mathematics Subject Classification ID

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

Recommendations

• Towards a unified ordering for superposition-based automated reasoning
• scientific article; zbMATH DE number 1405624
• scientific article; zbMATH DE number 1182797
• Maximal extensions of simplification orderings
• scientific article; zbMATH DE number 1980932

Cites work

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

Cited in

(2)

• Towards a unified ordering for superposition-based automated reasoning
• Weighted Path Orders Are Semantic Path Orders

Describes a project that uses

Uses Software

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

This page was built for publication: Relaxed weighted path order in theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2209265)