Building proofs or counterexamples by analogy in a resolution framework

DOI10.1007/3-540-61630-6_3zbMath1427.68345OpenAlexW1506416681MaRDI QIDQ5235252

Christophe Bourely, Gilles Défourneaux, Nicolas Peltier

Publication date: 8 October 2019

Published in: Logics in Artificial Intelligence (Search for Journal in Brave)

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

zbMATH Keywords

model buildingsecond-order termsanalogyextended resolution

Mathematics Subject Classification ID

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

Related Items (2)

Analogy in Automated Deduction: A Survey ⋮ Partial matching for analogy discovery in proofs and counter-examples

Uses Software

• TPTP

Cites Work

• Computational approaches to analogical reasoning: A comparative analysis
• Equational problems and disunification
• Theorem proving with abstraction
• A method for simultaneous search for refutations and models by equational constraint solving
• Non-resolution theorem proving
• The TPTP problem library. CNF release v1. 2. 1
• A paradigm for reasoning by analogy
• Efficient second-order matching
• A method for building models automatically. Experiments with an extension of OTTER
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Building proofs or counterexamples by analogy in a resolution framework