Perfect Discrimination Graphs: Indexing Terms with Integer Exponents

DOI10.1007/978-3-642-14203-1_32zbMath1291.68324OpenAlexW1479881342MaRDI QIDQ5747777

Hicham Bensaid, Ricardo Caferra, Nicolas Peltier

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_32

Mathematics Subject Classification ID

Related Items (2)

Simplified handling of iterated term schemata ⋮ A complete superposition calculus for primal grammars

Uses Software

• SPIKE
• E Theorem Prover
• Waldmeister

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Logic programming and automated reasoning. International conference, LPAR `92, St. Peterburg, Russia, July 15--20, 1992. Proceedings
• Increasing model building capabilities by constraint solving on terms with integer exponents
• Unification of infinite sets of terms schematized by primal grammars
• Implicit induction in conditional theories
• Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps
• On unification of terms with integer exponents
• Automated Reasoning

This page was built for publication: Perfect Discrimination Graphs: Indexing Terms with Integer Exponents