Simultaneous paramodulation

DOI10.1007/3-540-52885-7_106MaRDI QIDQ6488550zbMATH OpenFDO

Authors Dan Benanav

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_106

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1348470
• Basic paramodulation
• Goal directed strategies for paramodulation
• scientific article; zbMATH DE number 3837990
• On paramodulation in linear strategies of the resolution method

Cites work

• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Complete Sets of Reductions for Some Equational Theories
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)

Cited in

(17)

• Nonequivalence of input paramodulation refutation and unit paramodulation refutation
• Basic paramodulation
• Superposition with first-class booleans and inprocessing clausification
• Superposition for full higher-order logic
• Paramodulation-based theorem proving
• scientific article; zbMATH DE number 3837990 (Why is no real title available?)
• On paramodulation in linear strategies of the resolution method
• Paramodulation with non-monotonic orderings and simplification
• scientific article; zbMATH DE number 4022665 (Why is no real title available?)
• scientific article; zbMATH DE number 4049136 (Why is no real title available?)
• scientific article; zbMATH DE number 1763411 (Why is no real title available?)
• scientific article; zbMATH DE number 2090319 (Why is no real title available?)
• Implementing Superposition in iProver (System Description)
• Goal directed strategies for paramodulation
• Local simplification
• A comprehensive framework for saturation theorem proving
• Superposition for higher-order logic

This page was built for publication: Simultaneous paramodulation

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