An algorithm for the retrieval of unifiers from discrimination trees

DOI10.1007/3-540-61630-6_2zbMath1427.68346OpenAlexW1491223654MaRDI QIDQ5235251

Hans de Nivelle

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_2

zbMATH Keywords

implementationautomated theorem proving

Mathematics Subject Classification ID

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

Uses Software

• OTTER

Cites Work

• Experiments with discrimination-tree indexing and path indexing for term retrieval
• On a bound for the complexity of terms in the resolution method
• Resolution Strategies as Decision Procedures
• Extended path-indexing
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An algorithm for the retrieval of unifiers from discrimination trees