Partial matching for analogy discovery in proofs and counter-examples

DOI10.1007/3-540-63104-6_43zbMath1430.68398OpenAlexW1599030381MaRDI QIDQ5234724

Nicolas Peltier, Gilles Défourneaux

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_43

zbMATH Keywords

theorem provingpartial matchingequational formulapredicate symbolanalogy discovery

Mathematics Subject Classification ID

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

Related Items (2)

Proving theorems by reuse ⋮ Analogy in Automated Deduction: A Survey

Uses Software

• OTTER
• TPTP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equational problems and disunification
• A method for simultaneous search for refutations and models by equational constraint solving
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Non-resolution theorem proving
• The TPTP problem library. CNF release v1. 2. 1
• Efficient second-order matching
• Building proofs or counterexamples by analogy in a resolution framework

This page was built for publication: Partial matching for analogy discovery in proofs and counter-examples