ARCADE 2017: Papers with Abstracts

Abstract. The ARCADE workshop took place on the 6th August 2017 in Gothenburg, colocated with CADE-26. ARCADE stands for Automated Reasoning: Challenges, Applications, Directions, Exemplary achievements. The goal of this workshop was to bring together key people from various sub-communities of automated reasoning—such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving—to discuss the present, past, and future of the field.
The workshop was attended by 45 people and consisted of 14 short presentations and 5 discussion sessions. The format was informal and highly interactive. This report gives a general overview of the presentations and summarizes the discussion sessions.

Abstract. Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but with common interests, e.g., in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of the SC-square initiative is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications.

Abstract. We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.

Abstract. We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project, funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.

Abstract. Reasoning and learning have been considered fundamental features of intelligence ever since the dawn of the field of artificial intelligence, leading to the development of the research areas of automated reasoning and machine learning. This short paper is a non-technical position statement that aims at prompting a discussion of the relationship between automated reasoning and machine learning, and more generally between automated reasoning and artificial intelligence. We suggest that the emergence of the new paradigm of XAI, that stands for eXplainable Artificial Intelligence, is an opportunity for rethinking these relationships, and that XAI may offer a grand challenge for future research on automated reasoning.

Abstract. The greatest source of progress in automated theorem proving in the last 30 years has been the development of better search heuristics, usually based on developer experience and empirical evaluation, but increasingly also using automated optimization techniques. Despite this progress, we still know very little about proof search. We have mostly failed to identify good features for characterizing homogeneous problem classes, or for identifying interesting and relevant clauses and formulas.
I propose the challenge of bringing together inductive techniques (generalization and learning) and deductive techniques to attack this problem. Hardware and software have finally evolved to a point that we can reasonably represent and analyze large proof searches and search decisions, and where we can hope to achieve order-of-magnitude improvements in the efficiency of the proof search.

Abstract. This text briefly discusses and criticizes the prevailing attitudes towards AI and Machine Learning research in the current Automated Reasoning (CADE/IJCAR) community.

Abstract. Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, complex properties, where the verification process is based on logical inference. We list the most important challenges for the further development of the field.

Abstract. Industrial applications of interactive theorem proving dates back to the eighties. Enabling and achieving industrial successes has been an important focus of the ACL2 community. The ARCADE call-for-papers appears to ignore these results and the potential of automated reasoning in industry in the future. We briefly describe the penetration of the ACL2 theorem proving system into the microprocessor industry, list some of milestones achieved, the obstacles standing in the way, and some future research directions.

Abstract. Contemporary SAT solvers are complex tools and may contain bugs. In
order to increase the trust in the results of SAT solving, SAT solvers
may produce certificates that can be checked independently. For
unsatisfiability certificates, DRAT is the de facto standard. As long
as the checkers are not formalized, extending the certificate format
would decrease the trust in the checker because its code complexity
increases. With the advent of formally verified checkers for DRAT
proofs, this is no longer the case. In this note I argue that
symmetry breaking is not adequately supported by DRAT proofs, and
propose to have dedicated certification for symmetry breaking instead.

Abstract. In our extended abstract, we try to motivate researchers to investigate the potential of proof systems that modify a given set of formulas (e.g., a set of clauses in propositional logic) in a way that preserves satisfiability but not necessarily logical equivalence. We call such modifications interferences, because they
can change the models of a given set of formulas.

Abstract. Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),
we argue that a similar goal of having unified automatically checkable proofs should be sought
by the developers of automated first-order theorem provers (ATPs). This would not only
help to further increase assurance about the correctness of prover results,
but would also be indispensable for tools which rely on ATPs,
such as ``hammers'' employed within interactive theorem provers.
The current situation, represented by the TSTP format is unsatisfactory,
because this format does not have a standardised semantics and thus cannot be checked automatically.
Providing such semantics, however, is a challenging endeavour. One would ideally
like to have a proof format which covers only-satisfiability-preserving operations such as Skolemisation
and is versatile enough to encompass various proving methods (i.e. not just superposition)
or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.
Going beyond pure first-order logic to theory reasoning in the style of SMT or
beyond proofs to certification of satisfiability are further interesting challenges.
Although several projects have already provided partial solutions in this direction,
we would like to use the opportunity of ARCADE to further promote the idea and
gather critical mass needed for its satisfactory realisation.

Abstract. Answer Set Programming (ASP) has emerged as a successful paradigm for developing intelligent applications. ASP is based on adding negation as failure to logic programming under the stable model semantics regime. ASP allows for sophisticated reasoning mechanisms that are employed by humans to be modeled elegantly. We argue that being able to model common sense reasoning as used by humans is critical for success of automated reasoning. We also argue that extending answer programming systems to general predicates is critical to realizing the full power of ASP. Goal-directed predicate ASP systems are needed to make the ASP technology practical for building large, scalable knowledge-based applications.

Abstract. A number of synthesis applications are made possible by automated tools for synthesis. Recent work has shown that SMT solvers, instead of just acting as subroutines for automated software synthesis tasks, can be instrumented to perform synthesis themselves. This paper focuses on some of the current challenges for developing fast and useful procedures in SMT solvers for the benefit of synthesis applications.

Abstract. I discuss the question whether portfolio solvers support advances in automated reasoning.
A portfolio solver is the combination of a collection of core solvers.
I distinguish syntactic combinations from semantic combinations and argue
that the former are useful for competitions where the latter foster
progress in automated reasoning.