The paper presents an informal overview of the Connection Method in Automated Deduction. In particular, it points out its unique advantage over competing methods which consists in its formula-orientedness. Among the consequences of this unique feature are three striking advantages, viz. uniformity (over many logics), performance (due to its extreme compactness and goal-orientedness, evidenced by the leanCoP family of provers), and a global view over the proof process (enabling a higher-level guidance of the proof search). These aspects are discussed on the basis of the extensive work accumulated in the literature about this proof method. Along this line of research we envisage a bright future for the field and point out promising directions for future research.
CITATION STYLE
Bibel, W. (2017). A vision for automated deduction rooted in the connection method. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10501 LNAI, pp. 3–21). Springer Verlag. https://doi.org/10.1007/978-3-319-66902-1_1
Mendeley helps you to discover research relevant for your work.