@INPROCEEDINGS{ZoharTishkovskyEtAl19,
AUTHOR = {Zohar, Y. and Tishkovsky, D. and Schmidt, R. A. and Zamansky, A.},
YEAR = {2019},
TITLE = {Automating Automated Reasoning: The Case of Two Generic Automated Reasoning Tools},
EDITOR = {Lutz, C. and Sattler, U. and Tinelli, C. and Turhan, A.-Y. and Wolter, F.},
BOOKTITLE = {Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {11560},
PUBLISHER = {Springer},
PAGES = {610--638},
DOI = {10.1007/978-3-030-22102-7\_29},
NOTE = {Invited paper},
ABSTRACT = {
The vision of automated support for the investigation of logics, 
proposed decades ago, has been implemented in many forms, producing 
numerous tools that analyze various logical properties (e.g., 
cut-elimination, semantics, and more). However, full ‘automation of 
automated reasoning’ in the sense of automatic generation of 
efficient provers has remained a ‘holy grail’ of the field. 
Creating a generic prover which can efficiently reason in a given 
logic is challenging, as each logic may be based on a different 
language, and involve different inference rules, that require 
different implementation considerations to achieve efficiency, or 
even tractability. Two recently introduced generic automated provers 
apply different approaches to tackle this challenge. MetTeL, based 
on the formalism of tableaux, automatically generates a prover for
a given tableau calculus, by implementing generic proof-search 
procedures with optimizations applicable to many tableau calculi. 
Gen2sat, based on the formalism of sequent calculi, shifts the burden 
of search to the realm of off-the-shelf SAT solvers by applying a 
uniform reduction of derivability in sequent calculi to SAT. This 
paper examines these two generic provers, focusing in particular on 
criteria relevant for comparing their performance and usability. To 
this end, we evaluate the performance of the tools, and describe 
the results of a preliminary empirical study where user experiences 
of expert logicians using the two tools are compared.
},
}