Automatic acquisition of search control knowledge from multiple proof attempts.

DOI10.1006/inco.1999.2857zbMath1045.68602OpenAlexW2063042596MaRDI QIDQ1854367

Stephan Schulz, Jörg Denzinger

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/1815984bb4e462d8d51a09b1e77fd4c2bfbc5c6b

zbMATH Keywords

DISCOUNTdistributed equational proof system

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• TPTP
• DISCOUNT

Cites Work

• Unnamed Item
• Unnamed Item
• Recording and analysing knowledge-based distributed deduction processes
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Learning domain knowledge to improve theorem proving
• Experiments in the heuristic use of past proof experience
• Distributing equational theorem proving
• The TPTP problem library

This page was built for publication: Automatic acquisition of search control knowledge from multiple proof attempts.