ABSTRACT. TBA

ABSTRACT. We explore the integration of human intuition into automated reasoning systems by introducing aninterface language that enables a human expert to generate a multitude of conjectures from theoriginal problem statement. These conjectures are then utilized by an automated theorem prover todiscover new facts, thereby enriching the problem space. We evaluate the effectiveness of thisapproach on a number of problems from the TPTP library. Experimental results show that especiallythe combination of predicates and functions occurring in a problem file frequently producesbeneficial conjectures. Subsequently, we test the applicability of this form of conjecturing in anon-targeted context on a large number of problems.

ABSTRACT. We describe the implementation of first-order terms, the central data structure of most modernautomated theorem provers, as perfectly shared immutable term DAGs in E. We demonstrate typicalgains possible with this structure (reducing the number of term nodes typically by orders ofmagnitude) and discuss some of the side benefits of such a represen- tation. One of these benefitsis the ability to easily implement cached rewriting, improving the performance of rewriting-basedsimplification. We discuss lessons learned and some potential future work.

ABSTRACT. The E automated theorem proving system has an “automatic” mode that analyzes the input problem in order to choose an effective proof search strategy. A strategy includes the term/literal orderings, given clause selection heuristics, and a number of other parameters. This paper investigates the idea of creating one strategy for a given dataset of problems by merging the strategies chosen by E’s automatic mode over all of the problems in the dataset. This strategy merging approach is evaluated on the MPTPTP2078, VBT, and SLH-29 datasets. Surprisingly, the merged strategies outperform E’s automatic mode overall three datasets.

ABSTRACT. StarExec has been central to much progress in logic solvers over the last 10 years. It was recently announced that StarExec Iowa will be decommissioned, and while StarExec Miami will continue to operate while funding is available, it will not be able to support all the logic solver communities currently using the larger StarExec Iowa. In the long term StarExec will necessarily have to migrate to new compute environments. This paper describes work being done to reengineer StarExec as a cloud-native application using container technology and infrastructure-as-code practices. The first step has been to containerise StarExec and ATP systems so that they can be run on a broad range of computer platforms. The next step in process is to write a new backend in StarExec so that Kubernetes can be used to orchestrate distribution of StarExec job pairs over whatever compute nodes are available. Supported by an Amazon Research Award, a new version of StarExec will be deployed in AWS.