Using hints to increase the effectiveness of an automated reasoning program: Case studies

DOI10.1007/BF00252178zbMath0857.68095MaRDI QIDQ1923820

Robert Veroff

Publication date: 13 October 1996

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

zbMATH Keywords

hints strategyuser-supplied hint clause

Mathematics Subject Classification ID

Related Items

Finding proofs in Tarskian geometry, Fast and slow enigmas and parental guidance, ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Towards finding longer proofs, Learning theorem proving components, Axiomatizing the skew Boolean propositional calculus, Lemmatization for Stronger Reasoning in Large Theories, Shortest axiomatizations of implicational S4 and S5, MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance, Learning-assisted theorem proving with millions of lemmas, Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction, Toward a Procedure for Data Mining Proofs, Machine learning guidance for connection tableaux, Heaps and Data Structures: A Challenge for Automated Provers, Internal Guidance for Satallax, Proofs as schemas and their heuristic use, The application of automated reasoning to formal models of combinatorial optimization, A Wos Challenge Met, A posthumous contribution by Larry Wos: excerpts from an unpublished column, Guiding an automated theorem prover with neural rewriting, Double-negation elimination in some propositional logics

Uses Software

• OTTER
• AURA
• NQTHM

Cites Work

• Problem corner: Robbins algebra: Conditions that make a near-Boolean algebra Boolean
• Meeting the challenge of fifty years of logic
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• The linked inference principle. I: The formal treatment
• Complexity and related enhancements for automated theorem-proving programs
• Non-resolution theorem proving
• The resonance strategy
• Unnamed Item
• Unnamed Item
• Unnamed Item