Automatic acquisition of search control knowledge from multiple proof attempts.

DOI10.1006/INCO.1999.2857MaRDI QIDQ1854367zbMATH OpenOpenAlexFDO

Authors Jörg Denzinger, Stephan Schulz

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)

Recommendations

• scientific article; zbMATH DE number 1882060
• Automatic Learning of Proof Methods in Proof Planning
• Learning search control-knowledge for equational deduction
• Human-centered automated proof search
• scientific article; zbMATH DE number 1737186
• scientific article; zbMATH DE number 2101984
• Automata theoretic account of proof search
• Automating the search for elegant proofs
• Acquiring search-control knowledge via static analysis

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Distributing equational theorem proving
• Experiments in the heuristic use of past proof experience
• Learning domain knowledge to improve theorem proving
• Recording and analysing knowledge-based distributed deduction processes
• The TPTP problem library

Cited in

(8)

• scientific article; zbMATH DE number 1737186 (Why is no real title available?)
• Acquiring search-control knowledge via static analysis
• scientific article; zbMATH DE number 1882060 (Why is no real title available?)
• scientific article; zbMATH DE number 1552520 (Why is no real title available?)
• scientific article; zbMATH DE number 3982558 (Why is no real title available?)
• scientific article; zbMATH DE number 4047193 (Why is no real title available?)
• scientific article; zbMATH DE number 2086860 (Why is no real title available?)
• Experiments in the heuristic use of past proof experience

Describes a project that uses

Uses Software

• TPTP
• DISCOUNT

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

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