|Title||Tuning Natural Deduction Proof Search by Analytic Methods|
|Authors||Bolotov, A. and Gorchakov, A.|
This paper is a result of the analysis of the efficiency of natural deduction proof search and the
major weaknesses affecting it. We introduce new analytic strategies based on a new concept ”Truth Set of
Support”. We present a combined proof search algorithm for classical propositional logic where a crucially
new step is the guidance of the searching procedure by ”Truth sets of Support” and establish the correctness.
We describe the implementation of this new search technique and exemplify its advantages on the strong
version of the Pigeon Hole Principle.
|Keywords||automated deduction, natural deduction, pigeon hole principle|
|Conference||The 25th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice|
|Publisher||University of Cambridge|
|Accepted author manuscript|
File Access Level
Open (open metadata and files)
|Web address (URL) of conference proceedings||https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf|