A New Class of Automated Theorem-Proving Algorithms

DOI10.1145/321812.321814MaRDI QIDQ4773313zbMATH OpenOpenAlexFDO

Authors Ross A. Overbeek

Publication date 1974

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/321812.321814

Mathematics Subject Classification ID

Cited in

(10)

• Hierarchical deduction
• An implementation of hyper-resolution
• Non-resolution theorem proving
• Layered clause selection for theory reasoning (short paper)
• Guiding an automated theorem prover with neural rewriting
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Make E Smart Again (Short Paper)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Fast and slow enigmas and parental guidance

This page was built for publication: A New Class of Automated Theorem-Proving Algorithms

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