A New Class of Automated Theorem-Proving Algorithms

DOI10.1145/321812.321814zbMATH Open0286.68046OpenAlexW2063042358MaRDI QIDQ4773313FDOQ4773313

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)

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

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)