Stasys Lukaitis
email: stasys.lukaitis@rmit.edu.au

The Impact of the Y2K Event on the Popularity of the Pick Database Environment

Keywords: Pick, Universe, Unidata, Prime, Revelation, jBase, Reality, Multivalue, Correlative, D3, SAP, Oracle

At Pick's heyday there were over 3,000 business applications available across a very wide range of hardware platforms supporting from one to thousands of real time users. The tentative economic recovery of the 90s and the Y2K fears created cautious and conservative corporate decision-making. During those tumultuous years there were startling leaps in information and communications technology rewarding those who invested in the future and in themselves. The Pick community at the time were fragmented and somewhat narrow-minded in their view of the future and were unable to collectively invest in developing new technologies. Intense marketing by 'mainstream' relational database vendors combined with ERP software vendors brought executive peer group pressure to adopt 'vanilla' relational technologies and the desire for homogeneity and perceived immunity from the impending Y2K event. A new corporate jargon was developed to further seduce executive corporate decision makers.

Introduction

Decision making in ICT is rarely on the basis of cold hard logic or actual facts, but more often based on prejudice, comfort and expediency. Lots of decisions are sometimes made in the absence of, or despite important information. This paper seeks to highlight an interesting historical period in the development of Information and Communications Technology in Australia and to notice the various influences of (then) emerging factors on the Information Systems that were in use at that time, and the Pick Operating Systems and Database environment as an interesting example. The period under investigation is the last twenty years of the twentieth century 1980-2000, with the emphasis on the early 1990s and the period approaching the Y2K event.

A simple Google search for the PICK operating system or database will reveal a plethora of information about the history of the Pick Operating System and DBMS over the years. It is not the intention of this paper to repeat what is already freely available. Suffice it to say that PICK was 'invented' in the USA by Richard (Dick) Pick and Don Nelson as contractors for TRW on the Cheyenne Helicopter parts and maintenance project. This paper will look at the state of Information Systems that were in broad use during that period, the impact of the oncoming Y2K event, and the emergence of American and German software juggernauts Oracle and SAP and why they appeared to win the hearts, minds and wallets of enterprises across the globe.

Research Approach

This is a hermeneutical analysis of a brief period in Australian IT history using firsthand knowledge of the Pick environment and being an actor in that period as the driver. Hermeneutics is a philosophy of enquiry that seeks to gain understanding about an issue or question using techniques that attempt to deal with a researcher's biases and prejudices, and in particular the effects of historicality 1 -not taking into consideration the historical milieu and social events and thinking of the time, and the way that language and its use and interpretations can colour understanding and interpretation [START_REF] Gadamer | The Historicity of Understanding[END_REF].

In this usage of hermeneutics I use original documents in the form of books, reports, magazines, articles, quotations from the industry leaders of the time, reflections from practitioners and personal experience [START_REF] Lukaitis | Investigating Business and IT Alignment[END_REF]. The reason for the use of the hermeneutic philosophy is to glean understanding of the historical milieu from a variety of data sources. This research will review the 'forgotten factors' of the time, the drivers that pushed the Australian IT industry, the key decision makers and what was happening to technology then. Historical investigations such as this should be free from the emotion and biases because, as Gadamer stated, the passage of time has allowed the events to be 'closed' [START_REF] Gadamer | Truth and Method[END_REF].

The understanding and appreciation of history in its unsanitised form can be helpful in avoiding mistakes and errors already committed. It is a fact that with "all histories they are the tales of the winners who always rewrite history to their image, leaving many stories untold" [START_REF] Forrester | [END_REF].

A Quick Summary of the 'PICK' Concept

Unless one was versed in the idea of 'Pick', there was general confusion about what 'Pick' was. This is quite understandable because one's vision and potential comprehension is governed by knowledge, experience and a suitable vocabulary (set of paradigms) with which to understand and articulate that understanding.

Operating systems in the 1970s and 1980s were mostly proprietary and nonportable between hardware platforms. As an example, HP minicomputers were released with a proprietary operating system called MPE-IV (1980s) [START_REF] Hewlett-Packard | MPE-IV Software Pocket Guide[END_REF] that only worked on HP manufactured equipment. Similar examples existed with IBM and DEC (VMS).

Open systems were emerging and one called Unix was starting to be seen available on several different hardware platforms. This portability was exciting the ICT 1 Historicality: A term coined by Hans Georg Gadamer to describe the effect of time and cultural distance between the investigator and that being investigated. An example might be the difficulty in understanding life in ancient Rome from the perspective of a 21 st century New Yorker. community at the time because being tied to a particular hardware vendor was seen as undesirable for many reasons, one of which was being locked into a scalability ceiling 2 . IBM was famous at that time by offering relatively continuous scalability solutions right through to their mainframe systems.

It was quite normal for hardware vendors to also package their own proprietary operating system as a bundle resulting in the prevailing idea of an 'IBM' solution or 'HP' solution.

This section briefly outlines the Pick environment from four perspectives of a) the data model; b) the operating system; c) applications development environment; and d) the data retrieval model. Readers interesting in a more thorough explanation of this environment are referred to the bibliography for a range of material.

The Data Model

The actual database was modeled as a 'Hashed Indexed Sequential Access Method' (HSAM) mechanism. Each data record was indexed by a unique primary key that is used to calculate which frame (or bucket) is its home location inside a given fixedsize file. So for a given file and frame the read and write commands 'compiled' directly to an absolute disk, head and sector address.

Unlike other data models Pick's record structure is not predetermined by a Data Definition Language. Traditionally a database is created with the required number of tables, each table having its own peculiar structure. In Pick, one created files as needed, each one equivalent to a table. The database was then all the files that were related. Typically one would create an account called 'Student Records' and all the related files would be stored there.

Pick differs from other database models because it allows fields to have repeating values and for one field to be a 'controlling' field with others defined as 'dependent' fields. This allows alignment of repeating fields. It is also possible for any of these individual repeating fields to themselves store repeating 'sub-fields'.

Whereas people using the relational model must normalize their structures into strict two dimensional tables, the Pick model allows avoiding first normal form and the consequential join tables. Details of how Pick allowed data to be structured are well detailed by Lukaitis [START_REF] Lukaitis | A Short History of the Pick Environment in Australia[END_REF].

Thus one of the key differentiators of the Pick data model is that each 'master record' can also contain all the detail elements associated with transactions on that record. There are many examples that illustrate that the Pick model allows quite complex data structures to be represented that even today, using a strict relational model, would create very cumbersome join table proliferation and consequential management and expensive index maintenance collateral issues.

The Operating System Model

There was a stranglehold by the major vendors on their proprietary hardware and attached host operating systems. IBM, HP and DEC were but a few of the major players. It is now of historical interest the difficulties that IBM found themselves in with OS360 described by Brooks [START_REF] Brooks | Mythical Man Month[END_REF].

The Pick operating system was multi-user and time-sharing with the ability to run dozens of serial users on an Intel 486 computer with 512k RAM and an RS232 expansion card. Pick was an early implementer of code reentrancy which enabled efficient working set management to be implemented [START_REF] Denning | The working set model for program behavior[END_REF].

Perhaps from the Pick perspective, two important events were the release of the RISC engine as popularised by the Motorola M68x and IBM RS6x series chipsets and the implementation of SCSI hard disk technology which allowed very fast disk access. Pick was ported to the M68xx chipset and arrived in Australia as the Wicat computer. This was one of many ports of the operating system.

It is wise to remember, however, that in those days random access memory was very expensive and CPU speeds were only just starting to become acceptable (by those standards). The emergence of SCSI 3 technology released the hard disk bottleneck and allowed really quite fast disk operations on the smaller departmentalsized machine.

Pick's ability to leverage very fast disks, its ability to move large amounts of data quickly on and off the hard disk was its strong point. When combined with an elegant multi-user code re-entrant operating system model it was found possible to run quite large numbers of real time users simultaneously.

Of course, all operations back then were using green screen 4 technology with serial I/O along quite slow RS232 communications links.

Applications Development Environment

The applications development environment was implemented with a programming language that was tightly integrated to the host operating system and the database management system. The language syntax included very sophisticated string manipulation capabilities and dynamic arrays that mimicked and implemented the database's fundamental record structure, and internal conversion routines that allowed quite advanced date and time manipulation.

Specialised syntax allowed rapid read/write access to any files that your security level allowed. You could read an individual record or even fields within that record. Locks could be applied on a record to prevent file integrity problems surfacing in a multi-user environment to the degree where an optimistic locking strategy could be programmed to avoid a race condition and ultimate deadlock occurring.

The language compiled to a p-code 5 that was remarkably efficient in a multi-user environment and later into native chipset executable code which increased execution 3 SCSI. Small Computer Systems Interface. A quite revolutionary interface design that allowed hard disks to perform at speeds normally associated with larger mainframe style channel architecture disks. speed markedly. It supported run-time relocation of subroutine code. This was keenly exploited by programmers storing the names of candidate subroutines in files that were read during program execution and loaded and run according to state conditions. Recursion was also supported, although not greatly used as it (still) is a dangerous tool in the hands of any novice programmer.

Most Pick developers were conscious of the power in the programming environment and took appropriate precautions. Nevertheless, as Dick Pick was once quoted as saying that his system was replete with features he called 'rope'. There was plenty there with which to hang yourself [START_REF] Rodstein | Pick For Professionals -Advanced Methods and Techniques[END_REF].

The only problem with this development environment and language was its name -Pick/BASIC. Most developers in the Pick community thought nothing of its name, but were constantly embroiled in bickering about the language with non-Pick developers who imagined it to be a form of Dartmouth Basic.

This unfortunate name was also responsible to large degree for its lack of acceptance, even derision by a 'sophisticated' academia who felt that anything called Basic was just that -Basic and too simplistic to even be considered. When this was compounded with a data base model that allowed non first normal form, a heresy at the time, the whole environment was simply discarded as irrelevant.

Pre SQL Environment

The query language, called ACCESS, used against a given file would be driven by the data dictionary associated with that file. In other words, using the student record example earlier, you could readily query the student file for reports or information from the target file name (student) and the list of fields (dictionary definitions) in which you were interested. This is consistent with most modern query languages such as SQL. Unlike modern day SQL, Pick ACCESS is strictly a reporting language.

The 1980s and 1990s Context

Database Choices

In those early days of databases there were several choices of database model. Indexed Sequential Access Model (ISAM) databases were the most popular amongst the larger machines and were used by IBM in their offerings and made 'famous' by the leading database writers of the time like James Martin [START_REF] Martin | Computer Database organization[END_REF]. The other popular database model at the time was the network model, a precursor to the relational model of today. This was popular amongst mini-computer vendors typified by Hewlett Packard and the IMAGE databases [START_REF] Volokh | Relational Databases vs IMAGE: What the Fuss is all About[END_REF].

The iconic Ted Codd published a number of papers describing the two-dimensional relational database model, based on predicate logic and a relational algebra and calculus [START_REF] Codd | A relational model of data for large shared data banks[END_REF][START_REF] Codd | Extending the database relational model to capture more meaning[END_REF][START_REF] Codd | The relational model for database management: version 2[END_REF]. Numerous implementations of this relational database were spawned with some examples being DB2, Informix, Ingres, Sybase, Unify, Progress, Oracle (various hardware platforms) and later, some Open Source Unix implementations such as PostreSQL and MySQL 6 .

Computer Science Departments' Impact

Universities around the world became enamoured of a DBMS that was based on a mathematical model. This was understandable as many computer science departments and their academics were born of mathematics schools [START_REF]Advanced College Handbook[END_REF].

Database courses were taught in Universities at the time used the popular book by Tsichritzis (Data Models) [START_REF] Tsichritzis | Data Models[END_REF] that identified three main data modelsthe relational, network and hierarchical models and further treated on the E-R 7 , Binary, Semantic and Infological models. These were the only models taught.

Only now it becomes evident that many of these computer science career academics did not have any real industrial or commercial exposure with real world databases. This lack of experience was manifested in the sorts of data models and environments that were used to demonstrate the power of the relational model.

The Drive away from Centralised DP Departments

Mainframes were becoming increasingly unpopular because of the hold by DP 8 departments on business applications development (COBOL, PL/I, RPGII, etc.) and delays and errors in delivery of systems. Anecdotal evidence at the time estimated the applications development lead time to be about 4 years. The inability of centralized DP departments to provide satisfactory service levels (sic) led to local 'Departmental' solutions leveraging off the emergence of the new mini-computers. Many of these solutions were sourced from enterprising companies who could see the need for bureaus, a service that companies or Departments could buy to solve pressing IT problems.

The same themes are emerging today with offshore development now quite popular, and the emergence of cloud computing that promises applications, infrastructure and even complex information systems solutions at the click of a mouse.

Accountants and Managers Freed from their DP Departments

Spreadsheets9 empowered the accounting fraternity with the ability to create complex budgets and perform 'what if' scenarios. This released accountants from the control of 6 MySQL: Bought out by Sun Microsystems which is now owned by Oracle. their DP groups and mainframe-based computer financial models and gave them the independence to plan, model and forecast without the constant DP engagement.

This independence from DP departments had a liberating effect on the executives of organisations. What became clear to them was that their DP people were not as critical as once thought; and that the corporate world did not collapse once these PCs were were deployed.

The Internet

The second thing after PCs and spreadsheets was international data communications, Usenet and email. In hindsight this event created the birth of the global village. By subscribing to your local ISP of the time you could plug into the wisdom of thousands of savants and exchange electronic mail with them and others instantly. Back in the 1980s some quite serious problems could be tackled by joining the appropriate user group and taking a few tentative steps in asking for help. Like today's Wikipedia and Web2.0 the newsgroups were dominated by the loudest and most shrill voices and those with the most apparent authority. It is not surprising then that many vendors spent considerable budget ensuring that their message was being received loud and clear.

It is also important to remember that the Internet of the 20 th century was not yet indexed as is today's Internet and search engines were still not even a dream. If you wanted information you needed to know where to get it. Vendors were very quick to see this Internet thing as a new marketing opportunity.

Australian SMEs

Because of simple scale factors, Australia had a lot of small to medium enterprises (SMEs) for whom mainframe solutions were inappropriate and who might have turned to a bureau solution. The new mini-computers [START_REF] Brinton | New minis push into power era[END_REF]18] became attractive options and were actively pursued. Companies whose IT was agile enough to 'move with the times' often gained significant competitive advantage by simply having better IT solutions than their competitors.

Examples of this were the burgeoning Credit Union movement in Australia, sophisticated Insurance and Library solutions, and very popular manufacturing and distribution systems reminiscent of the original TRW product and precursors to the MRP and MRP-II10 products.

In a later section I will mention the impact of 4 th generation languages. However, Australian SMEs took great advantage of the flexibility of the data model, the power of programming and reporting and the rapid applications development opportunities afforded by the these 4GL environments by developing bespoke applications that genuinely met their specific business needs.

Voices from the Australian Pick Community in 1992

The Australian Pick community was quite vibrant in those days, led mainly by competing vendors of specific Pick flavours. A snapshot of the conversations of the day identified surprisingly few controversies.

Peter Fenwick suggested that "Pick's future is rosy because of its acceptance of Unix (Open Systems) as a host operating system. Pick is far more efficient than its competitors so one can run more users on equivalent hardware" [START_REF] Fenwick | New Directions in Information Technology, in Pick-Up1992, International Pick Users Association[END_REF]. He was one of many who were moving away from Dick Pick's view that a hand written operating system was more powerful than Open Source (aka Unix in its various flavours). Rob Coulsen, a major reseller the time agreed and added that "Pick's success will be driven by its breadth of applications" [START_REF] Coulson | The Future of PIK in Australia, in Pick-Up1992, International Pick Users Association[END_REF].

Others like Terry Leister from vMark [START_REF] Leister | Where is Pick Going?[END_REF], Al Dei Maggi of Sequent [START_REF] Maggi | Pick -From Proprietary to open Systems[END_REF] and Charles Cave from Unidata [START_REF] Cave | Where is Pick Heading?[END_REF] also saw that a GUI (Graphical User Interface) was key to Pick's ongoing success. Tom Couvret of Prime [START_REF] Couvret | Pick -the Next 10 Years, in Pick-Up1992, International Pick Users Association[END_REF]. And Bob Highland of GA [START_REF] Highland | Whither Pick in the 90s?[END_REF] felt that the new data communications technologies needed to be addressed.

Many like Tim Chianti from Apscore [START_REF] Cianchi | Will Pick (and the software business as we know it) Survive?[END_REF], Mike Ferris from Unipix [START_REF] Ferris | Where is Pick Headed in the Next 5-10 Years?[END_REF] and John Buchanan of Triad [START_REF] Buchanan | Whither Pick or Wither Pick?[END_REF] all thought that Pick needed to embrace interoperability with SQL, the 'mainstream' relational database vendors as well as integration with the emerging Microsoft Office suite.

An interesting comment of that time was from Barry Churchill of the NRMA who stated "Pick must employ the principles of TQM in continually addressing seamless integration with today's (1992) technology. Pick needs to listen to its users to understand what their needs are. After all, it's the 'users' who will buy the business systems" [START_REF] Churchill | The future of Pick -a User's View[END_REF]. But a more light-hearted comment was made by Alan Glassman from BIX who suggested "Pick needed to be ported to the 'state-of-the-art' 3270/RJE and HASP protocols. Microsoft to re-introduce command line for Windows/LANMan and Client/Server systems. ADDS terminal division releases a toast-r-oven connection to their 9000 series terminal" [START_REF] Glassman | Predictions for 1992, in Pick-Up1992, International Pick Users Association[END_REF].

The recurring themes from the Pick community were that Pick as an operating system was doomed and that Unix was to be the host of the future. Interoperability with the burgeoning PC marketplace and other systems (RDBMS 11 ) was the next theme followed by the emerging industry standards such as SQL. Networking was addressed by some and its relative low profile in these discussions indicated how little the Pick community thought about TCP/IP, LANs and distributed databases.

Pick's Popularity

During the 1980s through to Y2K Pick boasted that it had more business solutions available than any other environment. There was even a publication called 'The Business Software Catalog' that detailed over 3,000 such business applications [START_REF] Idbma | Industry Impact Study -the Pick Marketplace[END_REF]. The vast library of systems written in Pick/BASIC could be ported from single user machines through to high-end symmetric multi-processors with redundant non-stop architecture capabilities supporting thousands of real-time users.

In addition there were several integrated development environments based on Pick called fourth generation languages (4GL) or CASE 12 tools that ranged from elementary program generators such as Wizard 13 to truly configuration and data driven enterprise-class engines such as Cuebic 14 , SB+ 15 and Posh 16 .

In the 1990s it was not uncommon for an organization to identify a software solution that it needed and to purchase (separately) the hardware platform upon which to mount an operating system (such as Unix), a version of Pick (such as Universe), a 4GL (such as Posh) and the accounting, finance and HR system written in Posh. The average CFO could not understand why it was possible to get everything from one shop on the one invoice, like with an IBM solution.

There was great end-user flexibility in the choices available and numerous vendors each able to supply the 'perfect solution'. The competition was consequently brisk and in high value cases, immensely pressured. The various 'Pick' vendors robustly vied with each other for the prize of the Operating System licence that was often tied to a hardware platform because of the limited ports made by that vendor.

The other edge of the sword was that when errors or difficulties arose it was often difficult to identify the culprithardware, operating system, DBMS, 4GL or applications software and it was not uncommon for each to blame the other.

Just Before Y2k

As the Y2K event approached, the 'mainstream' RDBMS community was mounting a major marketing campaign along with emerging larger software houses like SAP guaranteeing Y2K compliance and promising many years of trouble-free use with their 'best of breed' and 'world's best practice' products. This idea appealed to many 'C' level executives and a lot of organisations who were struggling with their legacy COBOL, RPGII and PL/1-based systems, elected to adopt typically SAP or Oracle solutions.

There was comfort in conforming to peer group pressure that was vigorously supported by so many seemingly knowledgeable people in so many forums. After all, if everyone was going that way then surely everyone can't be wrong?

The emergence of a new marketing jargon embracing such concepts as best of breed and world's best practice started to bite. It was commonplace then to hear these terms used by vendors who claimed them for themselves. Their international marketing penetration brought the use of these terms into the current corporate language, but most importantly, associated with their particular products.

Furthermore, these vendors bypassed the normal ICT decision-making processes by presenting their sales pitches to the senior executives like CEOs and CFOs bypassing the impotent IT and DP managers. Company directors were targeted directly through their associations, a practice just unknown amongst the Pick community.

What changed?

At the Y2K event on Saturday January 1 st 2000 the world did not end, electricity kept coming out of power points, water flowed as did gas. The IT community rejoiced in their collective wisdom and ability to prevent the disasters that were predicted. However, a number of important new influences or orthodoxies had emerged and had taken root…  Alignment between cost and value and quality:

o o Thousands of graduates have only ever been exposed to the Codd relational model and cannot conceive of other models. o Students are increasingly educated using artificial business models that neatly fit their relational toolkits and avoid real-world complexity. The Pick community was certainly not united. Even the local Victorian IPUA attempted to assuage their vendors' sensibilities by renaming themselves to the 'Multi-Dimensional Database Forum' to remove the word 'Pick' from the association name. Few licensees embraced TCP/IP and fewer still acknowledged SQL and interoperability, and those that did make such an investment ensured that it remained proprietary and certainly not portable to other Pick vendors.

Perhaps the most important, if not subtle change was how corporate ICT decision making had evolved. The vendors, both ERP and their associated database suppliers no longer dealt with anyone lower than the absolute top level decision makers. After all, why negotiate with an IT manager when they would have to put a submission to a higher authority.

Associated with this exclusion of the IT personnel is the windfall consequence of financial decisions being made with only the highest level decision-maker. The vendors are then only beholding to the boards of directors who have already been marketed at their associations such as the Australian Institute of Company Directors.

Conclusions

The Pick community's inability to work together on keeping up with technology will be one of the reasons that many organisations will be electing to drop Pick as their preferred business platform and select more expensive mainstream solutions.

It is my opinion that industry had become so used to the two dimensional database model that interfaces tended to mirror the spreadsheet in concept. Pick's data model being inherently three (or even four) dimensional was difficult to effectively represent with the tools of the day and it never made an effort to effectively market the innate advantage that such structures offered. It is of passing interest that today's advanced HTML is now capable of such a representation without too much difficulty.

It is also curious to note that no popular operating system has been named after its inventor. Had PickOS been named something like OSMV (OS Multi-value) then a lot of criticism might have been avoided, and many days in the California Superior Court likewise avoided. And had Dick Pick named his programming language similarly after the famous courtesans like Pascal and Ada, perhaps something like 'Zion' might have reduced the criticisms of the language name.

But it is perception that matters today and perception is reality. Perception is a controlled substance and today the accepted orthodoxies are Windows point and click, Internet, Unix, rigorous Codd relational model and it just has to be 'world's best practice', whatever that means. With senior executives independently making the key decisions today, businesses are happy to change their business models and processes to align with some 'best' standard from Europe or America as manifested in a small selection of 'Enterprise' systems. And thanks to the largest software manufacturer in the world, it doesn't necessarily have to work entirely properly either.

7 E

 7 -R: Entity Relationship data model.

8 DP:

 8 Data Processing departments as they were known at that time.

  The acceptance of products such as Oracle and SAP and their million dollar price tags by financial controllers seeking Y2K immunity. o How can something costing $150k possibly be as good as something costing $1.5m?  Microsoft establishes universal acceptability of faulty software:o The now infamous EULA states unequivocally that the software you have bought is not guaranteed to work…  A new corporate jargon emerges:o Multi-million dollar applications from Europe and the USA with labels such 'best of breed', 'world's best practice' and 'enterprise class'. o Would you be brave enough to argue against a product solution that was 'acknowledged the best of breed' for your industry sector?  Decision making on IT acquisitions went from the IT people to the accountants:o Accountants who have now been liberated from their IT departments are now calling the shots on high value IT decisions. o There is a growing atmosphere of suspicion about the justifiability of the huge Y2K expenditures[START_REF] Lukaitis | The key issues that impact on the successful alignment of business and its IT function[END_REF].  The Windows GUI is the only practical user interface to a computer.  The Internet (and TCP/IP) is now the accepted data communications orthodoxy.  Safety in numbers: o In the older days, nobody was ever sacked for buying IBM. o Corporate leaders meet and compare notes about their respective IT solutions.  Universities control the corporate thinking:

Scalability ceiling: Reaching the performance limits of the hardware/operating systems platform and being unable to sensibly expand beyond that capability.

Green Screen. Character oriented screens typically 80 characters by 24 rows. No graphical user interfaces or mice as pointing devices.

P-Code. Pseudo code. A code that was not unlike assembler, but was interpreted at runtime by the internal Pick OS engine, not a p-code compiler.

And later and more ubiquitous was LOTUS-123.

MRP: Materials and Resource Planningprecursors to modern ERP packages.

RDBMS: Relational Database Management System.

CASE: Computer Aided Software Engineering.

Wizard: An early program generator that 'created' PICK/Basic code from user entered parameters to describe transaction processes against Pick databases.

Cuebic: A name alluding to the three dimensional nature of the Pick data model.

SB+: System Builder plus.

Posh: An acronym for 'Port Out Starboard Home', the preferred window allocation on trans-Atlantic boat trips. The name was adopted by its designer and developer Warren Dickins, a boating enthusiast.


Haniel Barbosa
email: haniel.barbosa@loria.fr

Jasmin Christian Blanchette
email: jasmin.blanchette@loria.fr

Pascal Fontaine
email: pascal.fontaine@loria.fr

Pascal Fontaine Scalable

Scalable Fine-Grained Proofs for Formula Processing

Introduction

An increasing number of automatic theorem provers can generate certificates, or proofs, that justify the formulas they derive. These proofs can be checked by other programs and shared across reasoning systems. Some users will also want to inspect this output to understand why a formula holds. Proof production is generally well understood for the core proving methods and for many theories commonly used in satisfiability modulo theories (SMT). But most automatic provers also perform some formula processing or preprocessing-such as clausification and rewriting with theory-specific lemmas-and proof production for this aspect is less mature.

For most provers, the code for processing formulas is lengthy and deals with a multitude of cases, some of which are rarely executed. Although it is crucial for efficiency, this code tends to be given much less attention than other aspects of provers. Developers are reluctant to invest effort in producing detailed proofs for such processing, since this requires adapting a lot of code. As a result, the granularity of inferences for formula processing is often coarse. Sometimes, processing features are even disabled to avoid gaps in proofs, at a high cost in proof search performance.

Fine-grained proofs are important for a variety of applications. We propose a framework to generate such proofs without slowing down proof search. Proofs are expressed using an extensible set of inference rules (Sect. 3). The succedent of a rule is an equality between the original term and the translated term. (It is convenient to consider formulas a special case of terms.) The rules have a fine granularity, making it possible to cleanly separate theories. Clausification, theory-specific simplifications, and expansion of 'let' expressions are instances of this framework. Skolemization may seem problematic, but with the help of Hilbert's choice operator, it can also be integrated into the framework. Some provers provide very detailed proofs for parts of the solving, but we are not aware of any publications about practical attempts to provide easily reconstructible proofs for processing formulas containing quantifiers and 'let' expressions.

At the heart of the framework lies a generic contextual recursion algorithm that traverses the terms to translate (Sect. 4). The context fixes some variables, maintains a substitution, and keeps track of polarities or other data. The transformation-specific work, including the generation of proofs, is performed by plugin functions that are given as parameters to the framework. The recursion algorithm, which is critical for the performance and correctness of the generated proofs, needs to be implemented only once. Another benefit of the modular architecture is that we can easily combine several transformations in a single pass, without complicating the code unduly or compromising the level of detail of the proof output. For very large inputs, this can improve performance.

The inference rules and the contextual recursion algorithm enjoy many desirable properties (Sect. 5). We show that the rules are sound and that the treatment of binders is correct even in the presence of name clashes. Moreover, assuming suitable data structures, we show that proof generation adds an overhead that is proportional to the time spent processing the terms. Checking proofs represented as directed acyclic graphs (DAGs) can be performed with a time complexity that is linear in their size.

We implemented the approach in veriT (Sect. 6), an SMT solver that is competitive on problems combining equality, linear arithmetic, and quantifiers [START_REF] Barbosa | Congruence closure with free variables[END_REF]. Compared with other SMT solvers, veriT is known for its very detailed proofs [START_REF] Besson | A flexible proof format for SMT: A proposal[END_REF], which are reconstructed in the proof assistants Coq [START_REF] Armand | A modular integration of SAT/SMT solvers to Coq through proof witnesses[END_REF] and Isabelle/HOL [START_REF] Blanchette | Semi-intelligible Isar proofs from machine-generated proofs[END_REF] and in the GAPT system [START_REF] Ebner | System description: GAPT 2.0[END_REF]. As a proof of concept, we implemented a prototype checker in Isabelle/HOL.

By adopting the new framework, we were able to remove large amounts of complicated code in the solver, while enabling detailed proofs for more transformations than before. The contextual recursion algorithm had to be implemented only once and is more thoroughly tested than any of the monolithic transformations it subsumes. Our empirical evaluation reveals that veriT is as fast as before even though it now generates finer-grained proofs.

A shorter version of this report was presented at CADE-26 as a system description [?]. The current report includes more explanations and examples, detailed justifications of the metatheoretical claims, and extensive coverage of related work.

Conventions

Our setting is a many-sorted classical first-order logic as defined by the SMT-LIB standard [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF] or TPTP TFF [START_REF] Sutcliffe | The TPTP typed first-order form with arithmetic[END_REF]. Our results are also applicable to richer formalisms such as higher-order logic (simple type theory) with polymorphism [START_REF]Introduction to HOL: A Theorem Proving Environment for Higher Order Logic[END_REF]. A signature Σ = (S , F ) consists of a set S of sorts and a set F of function symbols over these sorts.

Nullary function symbols are called constants. We assume that the signature contains a Bool sort and constants true, false : Bool, a family ( : σ × σ → Bool) σ∈S of function symbols interpreted as equality, and the connectives ¬, ∧, ∨, and -→. Formulas are terms of type Bool, and equivalence is equality ( ) on Bool. Terms are built over function symbols from F and variables from a fixed family of infinite sets (V σ ) σ∈S . In addition to ∀ and ∃, we rely on two more binders: Hilbert's choice operator εx. ϕ and a 'let' construct, let xn sn in t, which simultaneously assigns n variables that can be used in the body t.

We use the symbol = for syntactic equality on terms and = α for syntactic equality up to renaming of bound variables. We reserve the names a, c, f, g, p, q for function symbols; x, y, z for variables; r, s, t, u for terms (which may be formulas); ϕ, ψ for formulas; and Q for quantifiers (∀ and ∃). We use the notations ān and (a i ) n i=1 to denote the tuple, or vector, (a 1 , . . . , a n ). We write [n] for {1, . . . , n}.

Given a term t, the sets of its free and bound variables are written FV(t) and BV(t), respectively. The notation t[ xn ] stands for a term that may depend on distinct variables xn ; t[ sn ] is the corresponding term where the terms sn are simultaneously substituted for xn . Bound variables in t are renamed to avoid capture. Following these conventions, Hilbert choice and 'let' are characterized by

|= ∃x. ϕ[x] -→ ϕ[εx. ϕ] (ε 1 ) |= (∀x. ϕ ψ) -→ (εx. ϕ) (εx. ψ) (ε 2 ) |= (let xn sn in t[ xn ]) t[ sn ] (let)
Substitutions ρ are functions from variables to terms such that ρ(x i ) = x i for at most finitely many variables x i . We write them as { xn → sn }; the omitted variables are mapped to themselves. The substitution ρ[ xn → sn ] or ρ[x 1 → s 1 , . . . , x n → s n ] maps each variable x i to the term s i and otherwise coincides with ρ. The application of a substitution ρ to a term t is denoted by ρ(t). It is capture-avoiding; bound variables in t are renamed as necessary. Composition ρ • ρ is defined as for functions (i.e., ρ is applied first).

Inference System

The inference rules used by our framework depend on a notion of context defined by the grammar

Γ ::= ∅ | Γ, x | Γ, xn → sn
The empty context ∅ is also denoted by a blank. Each context entry either fixes a variable x or defines a substitution { xn → sn }. Any variables arising in the terms sn will normally have been introduced in the context Γ on the left. If a context introduces the same variable several times, the rightmost entry shadows the others. Abstractly, a context Γ fixes a set of variables and specifies a substitution subst(Γ). The substitution is the identity for ∅ and is defined as follows in the other cases:

subst(Γ, x) = subst(Γ)[x → x] subst(Γ, xn → tn ) = subst(Γ) • { xn → tn }
In the first equation, the [x → x] update shadows any replacement of x induced by Γ.

The examples below illustrate this subtlety:

subst(x → 7, x → g(x)) = {x → g(7)} subst(x → 7, x, x → g(x)) = {x → g(x)}
We write Γ(t) to abbreviate the capture-avoiding substitution subst(Γ)(t).

Γ s t Γ t u TRANS if Γ(t) = t Γ s u Γ t i u i n i=1 CONG Γ f( tn ) f(ū n ) Γ, y, x → y ϕ ψ BIND if y / ∈ FV(Qx. ϕ) Γ (Qx. ϕ) (Qy. ψ) Γ, x → (εx. ϕ) ϕ ψ SKO ∃ Γ (∃x. ϕ) ψ Γ, x → (εx. ¬ ϕ) ϕ ψ SKO ∀ Γ (∀x. ϕ) ψ Γ r i s i n i=1 Γ, xn → sn t u LET if Γ(s i ) = s i for all i ∈ [n] Γ (let xn rn in t) u
• TAUT T relies on an oracle |= T to derive arbitrary lemmas in a theory T . In practice, the oracle will produce some kind of certificate to justify the inference. An important special case, for which we use the name REFL, is syntactic equality (up to renaming of bound variables); the side condition is then Γ(t) = α u. (We use = α instead of = because applying a substitution can rename bound variables.) • TRANS needs the side condition because the term t appears both on the left-hand side of (where it is subject to Γ's substitution) and on the right-hand side (where it is not). Without the side condition, the two occurrences of t in the antecedent could denote different terms. • CONG can be used for any function symbol f, including the logical connectives.

• BIND is a congruence rule for quantifiers. The rule also justifies the renaming of the bound variable (from x to y). The side condition prevents an unwarranted variable capture. In the antecedent, the renaming is expressed by a substitution in the context. If x = y, the context is Γ, x, x → x, which has the same meaning as Γ, x. • SKO ∃ and SKO ∀ exploit (ε 1 ) to replace a quantified variable with a suitable witness, simulating skolemization. We can think of the ε expression in each rule abstractly as a fresh function symbol that takes any fixed variables it depends on as arguments.

In the antecedents, the replacement is performed by the context. • LET exploits (let) to expand a 'let' expression. Again, a substitution is used. The terms rn assigned to the variables xn can be transformed into terms sn .

The antecedents of all the rules inspect subterms structurally, without modifying them. Modifications to the term on the left-hand side are delayed; the substitution is applied only in TAUT. This is crucial to obtain compact proofs that can be checked efficiently. Some of the side conditions may look computationally expensive, but there are ways to compute them fairly efficiently. Furthermore, by systematically renaming variables in BIND, we can satisfy most side conditions trivially, as we will prove in Sect. 5.

The set of rules can be extended to cater for arbitrary transformations that can be expressed as equalities, using Hilbert choice to represent fresh symbols if necessary. The usefulness of Hilbert choice for proof reconstruction is well known [START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF][START_REF] De Nivelle | Translation of resolution proofs into short first-order proofs without choice axioms[END_REF][START_REF] Paulson | Source-level proof reconstruction for interactive theorem proving[END_REF], but we push the idea further and use it to simplify the inference system and make it more uniform.

Example 1. The following derivation tree justifies the expansion of a 'let' expression:

CONG a a REFL x → a x a REFL x → a x a CONG x → a p(x, x) p(a, a) LET (let x a in p(x, x)) p(a, a)
It is also possible to further process the substituted term, as in this derivation:

TAUT + a + 0 a . . . CONG x → a p(x, x) p(a, a) LET (let x a + 0 in p(x, x)) p(a, a)
Example 2. The following derivation tree, in which ε x abbreviates εx. ¬ p(x), justifies the skolemization of the quantifier in the formula ¬ ∀x. p(x):

REFL x → ε x x ε x CONG x → ε x p(x) p(ε x ) SKO ∀ (∀x. p(x)) p(ε x ) CONG (¬ ∀x. p(x)) ¬ p(ε x )
The CONG inference above SKO ∀ is optional; we could have directly closed the derivation with REFL. In a prover, the term ε x would be represented by a fresh Skolem constant c, and we would ignore c's connection to ε x during proof search.

Skolemization can be applied regardless of polarity. Normally, we skolemize only positive existential quantifiers and negative universal quantifiers. However, skolemizing other quantifiers is sound in the context of proving. The trouble is that it is generally incomplete, if we introduce Skolem symbols and forget their definitions in terms of Hilbert choice. To paraphrase Orwell, all quantifiers are skolemizable, but some quantifiers are more skolemizable than others.

Example 3. The next derivation tree illustrates the interplay between the theory rule TAUT T and the equality rules TRANS and CONG:

CONG k k TAUT × 1×0 0 CONG k + 1×0 k + 0 TAUT + k + 0 k TRANS k + 1×0 k CONG k k CONG (k + 1×0 < k) (k < k)
We could extend the tree at the bottom with an extra application of TRANS and TAUT < to simplify k < k further to false. The example demonstrates that theories can be arbitrarily fine-grained, which often makes proof checking easier. At the other extreme, we could have derived (k + 1×0 < k) false using a single TAUT + ∪ × ∪ < inference.

Example 4. The tree below illustrates what can go wrong if we ignore side conditions:

REFL Γ 1 f(x) f(x) REFL Γ 2 x f(x) REFL Γ 3 p(y) p(f(f(x))) LET* Γ 2 (let y x in p(y)) p(f(f(x))) LET Γ 1 (let x f(x) in let y x in p(y)) p(f(f(x))) BIND (∀x. let x f(x) in let y x in p(y)) (∀x. p(f(f(x))))
In the above,

Γ 1 = x, x → x; Γ 2 = Γ 1 , x → f(x); and Γ 3 = Γ 2 , y → f(x). The inference marked with an asterisk (*) is illegal, because Γ 2 (f(x)) = f(f(x)) = f(x).
We exploit this to derive an invalid judgment, with a spurious application of f on the right-hand side. To apply LET legally, we must first rename the universally quantified variable x to a fresh variable z using the BIND rule:

REFL Γ 1 f(x) f(z) REFL Γ 2 x f(z) REFL Γ 3 p(y) p(f(z)) LET Γ 2 (let y x in p(y)) p(f(z)) LET Γ 1 (let x f(x) in let y x in p(y)) p(f(z)) BIND (∀x. let x f(x) in let y x in p(y)) (∀z. p(f(z)))
This time, we have

Γ 1 = z, x → z; Γ 2 = Γ 1 , x → f(z); and Γ 3 = Γ 2 , y → f(z). LET's side condition is satisfied: Γ 2 (f(z)) = f(z).
Example 5. The dangers of capture are illustrated by the following tree, where ε y stands for εy. p(x) ∧ ∀x. q(x, y):

REFL*
x, y → ε y (p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀x. q(x, ε y ))

SKO ∃
x (∃y. p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀x. q(x, ε y )) BIND (∀x. ∃y. p(x) ∧ ∀x. q(x, y)) (∀x. p(x) ∧ ∀x. q(x, ε y ))

The inference marked with an asterisk would be legal if REFL's side condition were stated using capturing substitution. The final judgment is unwarranted, because the free variable x in the first conjunct of ε y is captured by the inner universal quantifier on the right-hand side.

To avoid the capture, we rename the inner bound variable x to z. Then it does not matter if we use capture-avoiding or capturing substitution:

REFL x, y → ε y p(x) p(x) REFL x, y → ε y , x → z q(x, y) q(z, ε y ) BIND x, y → ε y (∀x. q(x, y)) (∀z. q(z, ε y )) CONG x, y → ε y (p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀z. q(z, ε y )) SKO ∃
x (∃y. p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀z. q(z, ε y )) BIND (∀x. ∃y. p(x) ∧ ∀x. q(x, y)) (∀x. p(x) ∧ ∀z. q(z, ε y ))

Contextual Recursion

We propose a generic algorithm for term transformations, based on structural recursion. The algorithm is parameterized by a few simple plugin functions embodying the essence of the transformation. By combining compatible plugin functions, we can perform several transformations in one traversal. Transformations can depend on some context that encapsulates relevant information, such as bound variables, variable substitutions, and polarity. Each transformation can define its own notion of context that is threaded through the recursion.

The output is generated by a proof module that maintains a stack of derivation trees. The procedure apply(R, n, Γ, t, u) pops n derivation trees Dn from the stack and pushes the tree

D 1 • • • D n R
Γ t u onto the stack. The plugin functions are responsible for invoking apply as appropriate.

The Generic Algorithm

The algorithm performs a depth-first postorder contextual recursion on the term to process. Subterms are processed first; then an intermediate term is built from the resulting subterms and is processed in turn. The context ∆ is updated in a transformation-specific way with each recursive call. It is abstract from the point of view of the algorithm.

The plugin functions are divided into two groups: ctx_let, ctx_quant, and ctx_app update the context when entering the body of a binder or when moving from a function symbol to one of its arguments; build_let, build_quant, build_app, and build_var return the processed term and produce the corresponding proof as a side effect. function process(∆, t) match t case x: return build_var(∆, x) case f( tn ):

∆ n ← (ctx_app(∆, f, tn , i)) n i=1 return build_app ∆, ∆ n , f, tn , (process(∆ i , t i )) n i=1 case Qx. ϕ: ∆ ← ctx_quant(∆, Q, x, ϕ) return build_quant(∆, ∆ , Q, x, ϕ, process(∆ , ϕ)) case let xn rn in t : ∆ ← ctx_let(∆, xn , rn , t ) return build_let(∆, ∆ , xn , rn , t , process(∆ , t ))

'Let' Expansion

The first instance of the contextual recursion algorithm expands 'let' expressions and renames bound variables systematically to avoid capture. Skolemization and theory simplification, presented below, assume that this transformation has been performed.

The context consists of a list of fixed variables and variable substitutions, as in Sect. 3. The plugin functions are as follows:

function ctx_let(Γ, xn , rn , t) return Γ, xn → (process(Γ, r i )) n i=1 function ctx_app(Γ, f, tn , i) return Γ function build_let(Γ, Γ , xn , rn , t, u) apply(LET, n+1, Γ, let xn rn in t, u) return u function build_app(Γ, Γ n , f, tn , ūn ) apply(CONG, n, Γ, f( tn ), f(ū n )) return f(ū n ) function ctx_quant(Γ, Q, x, ϕ) y ← fresh variable return Γ, y, x → y function build_quant(Γ, Γ , Q, x, ϕ, ψ) y ← Γ (x) apply(BIND, 1, Γ, Qx. ϕ, Qy. ψ) return Qy. ψ function build_var(Γ, x) apply(REFL, 0, Γ, x, Γ(x)) return Γ(x)
The ctx_let and build_let functions process 'let' expressions. In ctx_let, the substituted terms are processed further before they are added to a substitution entry in the context. In build_let, the LET rule is applied and the transformed term is returned. Analogously, the ctx_quant and build_quant functions rename quantified variables systematically. This ensures that any variables that arise in the range of the substitution specified by ctx_let will resist capture when the substitution is applied (cf. Example 4). Finally, the ctx_app, build_app, and build_var functions simply reproduce the term traversal in the generated proof; they perform no transformation-specific work.

Example 6. Following up on Example 1, assume ϕ = let x a in p(x, x). Given the above plugin functions, process(∅, ϕ) returns p(a, a). It is instructive to study the evolution of the stack during the execution of process. First, in ctx_let, the term a is processed recursively; the call to build_app pushes a nullary CONG step with succedent a a onto the stack. Then the term p(x, x) is processed. For each of the two occurrences of x, build_var pushes a REFL step onto the stack. Next, build_app applies a CONG step to justify rewriting under p: The two REFL steps are popped, and a binary CONG is pushed. Finally, build_let performs a LET inference with succedent ϕ p(a, a) to complete the proof: The two CONG steps on the stack are replaced by the LET step. The stack now consists of a single item: the derivation tree of Example 1.

Skolemization

Our second transformation, skolemization, assumes that 'let' expressions have been expanded and bound variables have been renamed apart. The context is a pair ∆ = (Γ, p), where Γ is a context as defined in Sect. 3 and p is the polarity (+, -, or ?) of the term being processed. The main plugin functions are those that manipulate quantifiers:

function ctx_quant((Γ, p), Q, x, ϕ) if (Q, p) ∈ {(∃, +), (∀, -)} then Γ ← Γ, x → sko_term(Γ, Q, x, ϕ) else Γ ← Γ, x return (Γ , p) function build_quant((Γ, p), ∆ , Q, x, ϕ, ψ) if (Q, p) ∈ {(∃, +), (∀, -)} then apply(SKO Q , 1, Γ, Qx. ϕ, ψ) return ψ else apply(BIND, 1, Γ, Qx. ϕ, Qx. ψ) return Qx. ψ
The polarity component of the context is updated by ctx_app, which is not shown. For example, ctx_app((Γ, -), ¬, ϕ, 1) returns (Γ, +), because if ¬ ϕ occurs negatively in a larger formula, then ϕ occurs positively. The plugin functions build_app and build_var are as for 'let' expansion.

Positive occurrences of ∃ and negative occurrences of ∀ are skolemized. All other quantifiers are kept as is. The sko_term function returns an applied Skolem function symbol following some reasonable scheme; for example, outer skolemization [START_REF] Nonnengart | Computing small clause normal forms[END_REF] creates an application of a fresh function symbol to all variables fixed in the context. To comply with the inference system, the application of SKO ∃ or SKO ∀ in build_quant instructs the proof module to systematically replace the Skolem term with the corresponding ε term when outputting the proof.

Example 7. Let ϕ = ¬ ∀x. p(x). The call process((∅, +), ϕ) skolemizes ϕ into ¬ p(c),
where c is a fresh Skolem constant. The initial process call invokes ctx_app on ¬ as the second argument, making the context negative, thereby enabling skolemization of ∀. The substitution x → c is added to the context. Applying SKO ∀ instructs the proof module to replace c with εx. ¬ p(x). The resulting derivation tree is as in Example 2.

Theory Simplification

All kinds of theory simplification can be performed on formulas. We restrict our focus to a simple yet quite characteristic instance: the simplification of u + 0 and 0 + u to u. We assume that 'let' expressions have been expanded. The context is a list of fixed variables. The plugin functions ctx_app and build_var are as for 'let' expansion (Sect. 4.2); the remaining ones are presented below:

function ctx_quant(Γ, Q, x, ϕ) return Γ, x function build_quant(Γ, Γ , Q, x, ϕ, ψ) apply(BIND, 1, Γ, Qx. ϕ, Qx. ψ) return Qx. ψ function build_app(Γ, Γ n , f, tn , ūn ) apply(CONG, n, Γ, f( tn ), f(ū n )) if f(ū n ) has form u+0 or 0+u then apply(TAUT + , 0, Γ, f(ū n ), u) apply(TRANS, 2, Γ, f( tn ), u) return u else return f(ū n )
The quantifier manipulation code, in ctx_quant and build_quant, is straightforward. The interesting function is build_app. It first applies the CONG rule to justify rewriting the arguments. Then, if the resulting term f(ū n ) can be simplified further into a term u, it performs a transitive chain of reasoning:

f( tn ) f(ū n ) u. Example 8. Let ϕ = k + 1 × 0 < k.
Assuming that the framework has been instantiated with theory simplification for additive and multiplicative identity, invoking process(∅, ϕ) returns the formula k < k. The generated derivation tree is as in Example 3.

Combinations of Transformations

Theory simplification can be implemented as a family of transformations, each member of which embodies its own set of theory-specific rewrite rules. If the union of the rewrite rule sets is confluent and terminating, a unifying implementation of build_app can apply the rules in any order until a fixpoint is reached. Moreover, since theory simplification modifies terms independently of the context, it is compatible with 'let' expansion and skolemization. This means that we can replace the build_app implementation from Sect. 4.2 or 4.3 with that of Sect. 4.4. In particular, this allows us to perform arithmetic simplification in the substituted terms of a 'let' expression in a single pass (cf. Example 1). The combination of 'let' expansion and skolemization is less straightforward. Consider the formula ϕ = let y ∃x.p(x) in y → y. When processing the subformula ∃x.p(x), we cannot (or at least should not) skolemize the quantifier, because it has no unambiguous polarity; indeed, the variable y occurs both positively and negatively in the 'let' expression's body. We can of course give up and perform two passes: The first pass expands 'let' expressions, and the second pass skolemizes and simplifies terms. The first pass also provides an opportunity to expand equivalences, which are problematic for skolemization.

There is also a way to perform all the transformations in a single instance of the framework. The most interesting plugin functions are ctx_let and build_var: function ctx_let((Γ, p), xn , rn , t)

for i = 1 to n do apply(REFL, 0, Γ, x i , Γ(r i ))

Γ ← Γ, xn → (Γ(r i )) n i=1 return Γ , p)
function build_var((Γ, p), x) apply(REFL, 0, Γ, x, Γ(x)) u ← process((Γ, p), Γ(x)) apply(TRANS, 2, Γ, Γ(x), u) return u

In contrast with the corresponding function for 'let' expansion (Sect. 4.2), ctx_let does not process the terms rn , which is reflected by the n applications of REFL, and it must thread through polarities. The call to process is in build_var instead, where it can exploit the more precise polarity information to skolemize the formula. The build_let function is essentially as before. The ctx_quant and build_quant functions are as for skolemization (Sect. 4.3), except that the else cases rename bound variables apart (Sect. 4.2). The ctx_app function is as for skolemization, whereas build_app is as for theory simplification (Sect. 4.4).

For the formula ϕ given above, process((∅, +), ϕ) returns (∃x. p(x)) → p(c), where c is a fresh Skolem constant. The substituted term ∃x. p(x) is put unchanged into the substitution used to expand the 'let' expression. It is processed each time y arises in the body y -→ y. The positive occurrence is skolemized; the negative occurrence is left as is. Using caching and a DAG representation of derivations, we can easily avoid the duplicated work that would arise if y occurred several times with positive polarity.

Scope and Limitations

Other possible instances of contextual recursion are the clause normal form (CNF) transformation and the elimination of quantifiers using one-point rules. CNF transformation is an instance of rewriting of Boolean formulas and can be justified by a TAUT Bool rule. Tseytin transformation can be supported by representing the introduced constants by the formulas they represent, similarly to our treatment of Skolem terms. One-point rules-e.g., the transformation of ∀x. x a -→ p(x) into p(a)-are similar to 'let' expansion and can be represented in much the same way in our framework. The rules for eliminating universal and existential quantifiers are as follows:

Γ s t Γ, x → t ϕ ψ 1PT ∀ if x / ∈ FV(s) and Γ(t) = t Γ (∀x. x s -→ ϕ) ψ Γ s t Γ, x → t ϕ ψ 1PT ∃ if x / ∈ FV(s) and Γ(t) = t Γ (∃x. x s ∧ ϕ) ψ
The plugin functions used by process would also be similar as those for 'let' expansion, except that detecting the assignment at ctx_quant requires examining the body of the quantified formula to determine whether the one-point rule is applicable.

Some transformations, such as symmetry breaking [START_REF] Déharbe | Exploiting symmetry in SMT problems[END_REF] and rewriting based on global assumptions, require a global analysis of the problem that cannot be captured by local substitution of equals for equals. They are beyond the scope of the framework. Other transformations, such as simplification based on associativity and commutativity of function symbols, require traversing the terms to be simplified when applying the rewriting. Since process visits terms in postorder, the complexity of the simplifications would be quadratic, while a processing that applies depth-first preorder traversal can perform the simplifications with a linear complexity. Hence, applying such transformations optimally is also outside the scope of the framework.

Theoretical Properties

Before proving any properties of contextual recursion or proof checking, we establish the soundness of the inference rules they rely on. We start by encoding the judgments in a well-understood theory of binders: the simply typed λ-calculus. A context and a term will be encoded together as a single λ-term. We call these somewhat nonstandard λ-terms metaterms. They are defined by the grammar

M ::= t | λx. M | (λ xn . M) tn
where x i and t i are of the same sort for each i ∈ [n]. A metaterm is either a term t decorated with a box , a λ-abstraction, or the application of an n-tuple of terms to an uncurried λ-abstraction that simultaneously binds n distinct variables. We let = αβ denote syntactic equality modulo αand β-equivalence (i.e., up to renaming of bound variables and reduction of applied λ-abstractions). We use the letters M, N, P to refer to metaterms. The notion of type is as expected for simply typed λ-terms: The type of t is the sort of t; the type of λx. M is σ → τ, where σ is the sort of x and τ the type of M; and the type of (λ xn . M) tn is the type of M. It is easy to see that all metaterms contain exactly one boxed term. M[t] denotes a metaterm whose box contains t, and M[N] denotes the same metaterm after its box has been replaced with the metaterm N.

Encoded judgments will have the form M N. The λ-abstractions and applications represent the context, whereas the box stores the term. To invoke the theory oracle |= T , we will need to reify equalities on metaterms-i.e., map them to equalities on terms. Let M, N be metaterms of type σ 1 → • • • → σ n → σ. We define reify(M N) as ∀ xn . t u, where M = αβ λx 1 . . . . λx n . t and N = αβ λx 1 . . . . λx n . u . Thanks to basic properties of the λ-calculus, t and u are always defined uniquely up to the names of the bound variables. For example, if M = λu. (λv. p(v) ) u and N = λw. q(w) , we have M = αβ λx. p(x) and N = αβ λx. q(x) , and the reification of M N is ∀x. p(x) q(x).

The inference rules presented in Sect. 3 can now be encoded as follows. We refer to these new rules collectively as the encoded inference system:

TAUT T if |= T reify(M N) M N M N N P TRANS if N = αβ N M P M[t i ] N[u i ] n i=1 CONG M[f( tn )] N[f(ū n )] M[λy. (λx. ϕ) y] N[λy. ψ] BIND if y / ∈ FV(Qx. ϕ) M[Qx. ϕ] N[Qy. ψ] M[(λx. ϕ) (εx. ϕ)] N SKO ∃ M[∃x. ϕ] N M[(λx. ϕ) (εx. ¬ ϕ)] N SKO ∀ M[∀x. ϕ] N M[r i ] N[s i ] n i=1 M[(λ xn . t) sn ] N[u] LET if M[s i ] = αβ N[s i ] for all i ∈ [n] M[let xn rn in t] N[u]
Lemma 1. If the judgment M N is derivable using the encoded inference system with the theories T 1 , . . . , T n , then |= T reify(M N) with

T = T 1 ∪ • • • ∪ T n ∪ ∪ ε ∪ let.
Proof. By structural induction on the derivation of M N. For each inference rule, we assume |= T reify(M i N i ) for each judgment M i N i in the antecedent and show that |= T reify(M N). Most of the cases implicitly depend on basic properties of the λ-calculus to reason about reify. CASE TAUT T : Trivial because T ⊆ T by definition of T . CASES TRANS, CONG, AND BIND: These follow from the theory of equality ( ). CASES SKO ∃ , SKO ∀ , AND LET: These follow from (ε 1 ) and (ε 2 ) or (let) and from the congruence of equality.

A judgment Γ t u is encoded as L(Γ)[t] R(Γ)[u],
where

L(∅)[t] = t R(∅)[u] = u L(x, Γ)[t] = λx. L(Γ)[t] R(x, Γ)[u] = λx. R(Γ)[u] L( xn → sn , Γ)[t] = (λ xn . L(Γ)[t]) sn R( xn → sn , Γ)[u] = R(Γ)[u]
The L function encodes the substitution entries of Γ as λ-abstractions applied to tuples.

Reducing the applied λ-abstractions effectively applies subst(Γ). For example:

L(x → 7, x → g(x))[x] = (λx. (λx. x ) (g(x))) 7 = αβ g(7) L(x → 7, x, x → g(x))[x] = (λx. λx. (λx. x ) (g(x))) 7 = αβ λx. g(x)
For any derivable judgment Γ t u, the terms t and u must have the same sort, and the metaterms L(Γ)[t] and R(Γ)[u] must have the same type. Another property is that L(Γ)[t] is of the form M[t] for some M that is independent of t and similarly for R(Γ) [ Incidentally, the converse of Lemma 3 does not hold, since the encoded inference rules allow metaterms that contain applied λ-abstractions on the right-hand side of .

Theorem 4 (Soundness of Inferences). If the judgment Γ t u is derivable using the original inference system with the theories T 1 , . . . , T n , then

|= T Γ(t) u with T = T 1 ∪ • • • ∪ T n ∪ ∪ ε ∪ let.
Proof. This follows from Lemmas 1 and 3. The equivalence of |= T Γ(t) u and |= T reify(L(Γ)[t] R(Γ)[u]) can be established along the lines of case TAUT T of Lemma 3.

We turn to the contextual recursion algorithm that generates derivations in that system. The first question is, Are the derivation trees valid? In particular, it is not obvious from the code that the side conditions of the inference rules are always satisfied. First, we need to introduce some terminology. A term is shadowing-free if nested binders always bind variables with different names; for example, ∀x. (∀y. p(x, y)) ∧ (∀y. q(y)) is shadowing-free, while ∀x. (∀x. p(x, y)) ∧ (∀y. q(y)) is not. The set of variables fixed by Γ is written fix(Γ), and the set of variables replaced by Γ is written repl(Γ). They are defined as follows:

fix(∅) = {} repl(∅) = {} fix(Γ, x) = {x} ∪ fix(Γ) repl(Γ, x) = repl(Γ) fix(Γ, xn → sn ) = fix(Γ) repl(Γ, xn → sn ) = {x i | s i = x i } ∪ repl(Γ)
Trivial substitutions x → x are ignored, since they have no effect. The set of variables introduced by Γ is defined by intr(Γ) = fix(Γ) ∪ repl(Γ). A context Γ is consistent if all the fixed variables are mutually distinct and the two sets of variables are disjoint-i.e., fix(Γ) ∩ repl(Γ) = {}.

A judgment Γ t u is canonical if Γ is consistent, FV(t) ⊆ intr(Γ), FV(u) ⊆ fix(Γ), and BV(u) ∩ intr(Γ) = {}. The canonical inference system is a variant of the system of Sect. 3 in which all judgments are canonical and rules TRANS, BIND, and LET have no side conditions. Lemma 5. Any inference in the canonical inference system is also an inference in the original inference system.

Proof. It suffices to show that the side conditions of the original rules are satisfied. CASE TRANS: Since the first judgment in the antecedent is canonical, FV(t) ⊆ fix(Γ). By consistency of Γ, we have fix(Γ) ∩ repl(Γ) = {}. Hence, FV(t) ∩ repl(Γ) = {} and therefore Γ(t) = t. CASE BIND: Since the succedent is canonical, we have ( 1) FV(Qx. ϕ) ⊆ intr(Γ) and ( 2) BV(Qy. ψ) ∩ intr(Γ) = {}. From (2), we deduce y / ∈ intr(Γ). Hence, by (1), we get y / ∈ FV(Qx. ϕ). CASE LET: Similar to TRANS.

Theorem 6 (Total Correctness of Recursion).

For the instances presented in Sects. 4.2 to 4.4, the contextual recursion algorithm always produces correct proofs.

Proof. The algorithm terminates because process is called initially on a finite input and recursive calls always have smaller inputs.

For the proof of partial correctness, only the Γ part of the context is relevant. We will write process(Γ, t) even if the first argument actually has the form (Γ, p) for skolemization. The pre-and postconditions of a process(Γ, t) call that returns the term u are

PRE1 Γ is consistent; PRE2 FV(t) ⊆ intr(Γ); PRE3 BV(t) ∩ fix(Γ) = {}; POST1 u is shadowing-free; POST2 FV(u) ⊆ fix(Γ); POST3 BV(u) ∩ intr(Γ) = {}.
For skolemization and simplification, we may additionally assume that bound variables have been renamed apart by 'let' expansion, and hence that the term t is shadowing-free.

The initial call process(∅, t) trivially satisfies the preconditions on an input term t that contains no free variable. We must show that the preconditions for each recursive call process(Γ , t ) are satisfied and that the postconditions hold at the end of process(Γ, t). PRE1 (Γ is consistent): First, we show that the fixed variables are mutually distinct. For 'let' expansion, all fixed variables are fresh. For skolemization and simplification, a precondition is that the input is shadowing-free. For any two fixed variables in Γ , the input formula must contain two quantifiers, one in the scope of the other. Hence, the variables must be distinct. Second, we show that fix(Γ ) ∩ repl(Γ ) = {}. For 'let' expansion, all fixed variables are fresh. For skolemization, the condition is a direct consequence of the precondition that the input is shadowing-free. For simplification, we have repl(Γ ) = {}.

PRE2 (FV(t ) ⊆ intr(Γ )):

We have FV(t) ⊆ intr(Γ). The desired property holds because the ctx_let and ctx_quant functions add to the context any bound variables that become free when entering the body t of a binder.

PRE3 (BV(t ) ∩ fix(Γ ) = {}):

The only function that fixes variable is ctx_quant. For 'let' expansion, all fixed variables are fresh. For skolemization and simplification, the condition is a consequence of the shadowing-freedom of the input. POST1 (u is shadowing-free): The only function that builds quantifiers is build_quant. The process(Γ , ϕ) call that returns the processed body ψ of the quantifier is such that y ∈ intr(Γ ) in the 'let' expansion case and x ∈ intr(Γ ) in the other two cases. The induction hypothesis ensures that ψ is shadowing-free and BV(ψ) ∩ intr(Γ ) = {}; hence, the result of build_quant (i.e., Qy. ψ or Qx. ψ) is shadowing-free. Quantifiers can also emerge when applying a substitution in build_var. This can happen only if ctx_let has added a substitution entry to the context, in which case the substituted term is the result of a call to process and is thus shadowing-free.

POST2 (FV(u) ⊆ fix(Γ)):

In most cases, this condition follows directly from the induction hypothesis POST2. The only case where a variable appears fixed in the context Γ of a recursive call to process and not in Γ is when processing a quantifier, and then that variable is bound in the result. For variable substitution, it suffices to realize that the context in which the substituted term is created (and which fixes all the free variables of the term) is a prefix of the context when the substitution occurs.

POST3 (BV(u) ∩ intr(Γ) = {}):

In most cases, this condition follows directly from the induction hypothesis POST3: For every recursive call, intr(Γ) ⊆ intr(Γ ). Two cases require attention. For 'let' expansion, a variable may be replaced by a term with bound variables. Then the substituted term only contains variables that do not occur in the input. The variables introduced by Γ will be other fresh variables or variables from the input. The second case is when a quantified formula is built. For 'let' expansion, a fresh variable is used. For skolemization and simplification, we have BV(Qx. ϕ) ∩ fix(Γ) = {} (PRE3); hence x / ∈ fix(Γ). Finally, we must show that x / ∈ repl(Γ); this is a consequence of the shadowing-freedom of the input.

It is easy to see that each apply call generates a rule with an antecedent and a succedent of the right form, ignoring the rules' side conditions. Moreover, all calls to apply generate canonical judgments thanks to the pre-and postconditions proved above. Correctness follows from Lemma 5.

Observation 7 (Complexity of Recursion).

For the instances presented in Sects. 4.2 to 4.4, the 'process' function is called at most once on every subterm of the input.

Justification. It suffices to notice that a call to process(∆, t) induces at most one call for each of the subterms in t.

As a corollary, if all the operations performed in process excluding the recursive calls can be accomplished in constant time, the algorithm has linear-time complexity with respect to the input. There exist data structures for which the following operations take constant time: extending the context with a fixed variable or a substitution, accessing direct subterms of a term, building a term from its direct subterms, choosing a fresh variable, applying a context to a variable, checking if a term matches a simple template, and associating the parameters of the template with the subterms. Thus, it is possible to have a linear-time algorithm for 'let' expansion and simplification.

On the other hand, construction of Skolem terms is at best linear in the size of the context and of the input formula in process. Hence, skolemization is at best quadratic in the worst case. This is hardly surprising because in general, the formula ∀x 1 . ∃y 1 . . . . ∀x n . ∃y n . ϕ[ xn , ȳn ], whose size is proportional to n, is translated to

∀x 1 . . . . ∀x n . ϕ[ xn , f 1 ( x1 ), f 2 ( x2 ), . . . , f n ( xn )], whose size is quadratic in n.
Observation 8 (Overhead of Proof Generation). For the instances presented in Sects. 4.2 to 4.4, the number of calls to the 'apply' procedure is proportional to the number of subterms in the input.

Justification. This is a corollary of Observation 7, since the number of apply calls per process call is bounded by a constant (3, in build_app for simplification).

Notice that all arguments to apply must be computed regardless of the apply calls. If an apply call takes constant time, the proof generation overhead is linear in the size of the input. To achieve this performance, it is necessary to use sharing to represent contexts and terms in the output; otherwise, each call to apply might itself be linear in the size of its arguments, resulting in a nonlinear overhead on the generation of the entire proof.

Observation 9 (Cost of Proof Checking). Checking an inference step can be performed in constant time if checking the side condition takes constant time.

Justification. The inference rules involve only shallow conditions on contexts and terms, except in the side conditions. Using suitable data structures with maximal sharing, the contexts and terms can be checked in constant time.

The above statement may appear weak, since checking the side conditions might itself be linear, leading to a cost of proof checking that can be at least quadratic in the size of the proof (measured as the number of symbols that represent it). Fortunately, most of the side conditions can be checked efficiently. For example, for simplification (Sect. 4.4), the BIND rule is always applied with x = y, which implies the side condition y / ∈ FV(Qx. ϕ); and since no other rule contributes to the substitution, subst(Γ) is the identity. Thus, simplification proofs can be checked in linear time. Moreover, certifying a proof by checking each step locally is not the only possibility. An alternative is to use an algorithm similar to the process function to check a proof in the same way as it has been produced. Such an algorithm can exploit sophisticated invariants on the contexts and terms.

Implementation

The ideas presented in this report have been implemented in two tools. We implemented the contextual recursion algorithm and the transformations described in Sect. 4 in the SMT solver veriT [START_REF] Bouton | veriT: An open, trustable and efficient SMT-solver[END_REF], showing that replacing the previous ad hoc code with the generic proof-producing framework had no significant detrimental impact on the solving times. In addition, we developed a prototypical proof checker for the inference system described in Sect. 3 using Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF], to convince ourselves that veriT's output can easily be reconstructed.

Isabelle

The Isabelle/HOL proof assistant is based on classical higher-order logic (HOL) [START_REF]Introduction to HOL: A Theorem Proving Environment for Higher Order Logic[END_REF], a variant of the simply typed λ-calculus. Thanks to the availability of λ-terms, we could follow the lines of the encoded inference system of Sect. 5 to represent judgments in HOL. The proof checker is included in the development version of Isabelle. 1Derivations are represented by a recursive datatype in Standard ML, Isabelle's primary implementation language. A derivation is a tree whose nodes are labeled by rule names. Rule TAUT T also carries a theorem that represents the oracle |= T , and rules TRANS and LET are labeled with the terms that occur only in the antecedent (t and sn ).

Terms and metaterms are translated to HOL terms, and judgments M N are translated to HOL equalities t u, where t and u are HOL terms. For example, the judgment x, y → g(x) f(y) f(g(x)) is represented by the HOL equality (λx. (λy. f y) (g x)) (λx. f (g x)). Uncurried λ-applications are encoded using a polymorphic combinator case × : (α → β → γ) → α × β → γ; in Isabelle/HOL, λ(x, y). t is syntactic sugar for case × (λx.λy. t). This scheme is iterated to support n-tuples, represented by nested pairs

(t 1 , (• • • (t n-1 , t n ) • • • )).
To implement the inference rules, it is necessary to be able to locate any metaterm's box. There is an easy criterion: Translated metaterms are of the form (λ. . . .) . . . or case × . . . , which is impossible for a translated term.

Because reconstruction is not verified, there are no guarantees that it will always succeed, but when it does, the result is certified by Isabelle's LCF-style inference kernel [START_REF] Gordon | Edinburgh LCF: A Mechanised Logic of Computation[END_REF]. We hard-coded a few dozen examples to test different cases, such as this one: Given the HOL terms t = ¬ ∀x. p ∧ ∃x. ∀x. q x x u = ¬ ∀x. p ∧ ∃x. q (εx. ¬ q x x) (εx. ¬ q x x)

and the ML tree

N (Cong, [N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_All, [N (Refl, [])])])])])]))
the reconstruction function returns the HOL theorem t u.

veriT

We implemented the contextual recursion framework in the SMT solver veriT,2 replacing large parts of the previous non-proof-producing, hard-to-maintain code. Even though it offers more functionality (proof generation), the preprocessing module is about 20% smaller than before and consists of about 3000 lines of code. There are now only two traversal functions instead of 10. This is, for us, a huge gain in maintainability.

Proofs Previously, veriT provided detailed proofs for the resolution steps performed by the SAT solver and the lemmas added by the theory solvers and instantiation module. All transformations performed in preprocessing steps were represented in the proof in a very coarse manner, amounting to gaps in the proof. For example, when 'let' expressions were expanded in a formula, the only information present in the proof would be the formula before and after 'let' expansion.

When extending veriT to generate more detailed proofs, we were able to reuse its existing proof module and proof format [START_REF] Besson | A flexible proof format for SMT: A proposal[END_REF]. A proof is a list of inferences, each of which consists of an identifier (e.g., .c0), the name of the rule, the identifiers of the dependencies, and the derived clause. The use of identifiers makes it possible to represent proofs as DAGs. We extended the format with the inference rules of Sect. 3. The rules that augment the context take a sequence of inferences-a subproof -as a justification. The subproof occurs within the scope of the extended context. Following this scheme, the skolemization proof for the formula ¬ ∀x. p(x) from Example 2 is presented as Formerly, no details of these transformations would be recorded. The proof would have contained only the original formula and the skolemized result, regardless of how many quantifiers appeared in the formula.

(.c0
In contrast with the abstract proof module described in Sect. 4, veriT leaves REFL steps implicit for judgments of the form Γ t t. The other inference rules are generalized to cope with missing REFL judgments. In addition, when printing proofs, the proof module can automatically replace terms in the inferences with some other terms. This is necessary for transformations such as skolemization and 'if-then-else' elimination. We must apply a substitution in the replaced term if the original term contains variables. In veriT, efficient data structures are available to perform this.

Transformations The implementation of contextual recursion uses a single global context, augmented before processing a subterm and restored afterwards. The context consists of a set of fixed variables, a substitution, and a polarity. In our setting, the substitution satisfies the side conditions by construction. If the context is empty, the result of processing a subterm is cached. For skolemization, a separate cache is used for each polarity. No caching is attempted under binders.

Invoking process on a term returns the identifier of the inference at the root of its transformation proof in addition to the processed term. These identifiers are threaded through the recursion to connect the proof. The proofs produced by instances of contextual recursion are inserted into the larger resolution proof produced by veriT. This is achieved through an inference of the form

ϕ D TAUT ¬ (ϕ ψ) ∨ ¬ ϕ ∨ ψ RESOLVE ψ
where ϕ is the original formula, ψ is the processed formula, and D is a derivation of ϕ ψ. The derivation D may itself depend on instances of rule TAUT T , each with its own proof of the side condition that must also be included in the overall proof.

Transformations performing theory simplification were straightforward to port to the new framework: Their build_app functions simply apply rewrite rules until a fixpoint is reached. Porting transformations that interact with binders required special attention in handling the context and producing proofs. Fortunately, most of these aspects are captured by the inference system and the abstract contextual recursion framework, where they can be studied independently of the implementation. Some transformations are performed outside of the framework. Proofs of CNF transformation are expressed using the inference rules of veriT's underlying SAT solver, so that any tool that can reconstruct SAT proofs can also reconstruct these proofs. Simplification based on associativity and commutativity of function symbols is implemented as a dedicated procedure, for efficiency reasons (Sect. 4.6). It currently produces coarse-grained proofs.

Evaluation To evaluate the impact of the new contextual recursion algorithm and of producing detailed proofs, we compare the performance of different configurations of veriT. Our experimental data is available online. 3 We distinguish three configurations. BASIC only applies transformations for which the old code provided some (coarsegrained) proofs. EXTENDED also applies transformations for which the old code did not provide any proofs, whereas the new code provides detailed proofs. COMPLETE applies all transformations available, regardless of whether they produce proofs.

More specifically, BASIC applies the transformations for 'let' expansion, skolemization, elimination of quantifiers based on one-point rules, elimination of 'if-then-else', theory simplification for rewriting n-ary symbols as binary, and elimination of equivalences and exclusive disjunctions with quantifiers in subterms. EXTENDED adds Boolean and arithmetic simplifications to the transformations performed by BASIC. COMPLETE performs global rewriting simplifications symmetry breaking in addition to the transformations in EXTENDED.

The evaluation was carried out on two main sets of benchmarks from SMT-LIB [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF]: the 20 916 benchmarks in the quantifier-free (QF) categories QF_ALIA, QF_AUFLIA, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL, QF_UFLIA, and QF_ UFLRA; and the 30 250 benchmarks labeled as unsatisfiable in the non-QF categories AUFLIA, AUFLIRA, UF, UFIDL, UFLIA, and UFLRA. The categories with bit vectors and nonlinear arithmetic are not supported by veriT. Our experiments were conducted on servers equipped with two Intel Xeon E5-2630 v3 processors, with eight cores per processor, and 126 GB of memory. Each run of the solver uses a single core. The time limit was set to 30 s, a reasonable value for interactive use within a proof assistant.

The tables below indicate the number of benchmark problems solved by each configuration for the quantifier-free and non-quantifier-free benchmarks: These results indicate that the new generic contextual recursion algorithm and the production of detailed proofs do not impact performance negatively in any significant way compared with the old code. The time difference is less than 0.1%, and the small changes in solved problems are within the difference one can observe when renaming symbols or reordering axioms. In addition, fine-grained proofs are now provided, whereas before only the original formula and the result were given after each set of transformations, without any further details, which arguably did not even constitute a proof.

Allowing Boolean and arithmetic simplifications leads to some improvements, especially for the quantifier-free benchmarks. We expect that generating proofs for the global transformations would lead to substantial improvements on these problems.

Related Work

Most automatic provers that support the TPTP syntax for problems generate proofs in TSTP (Thousands of Solutions for Theorem Provers) format [START_REF] Sutcliffe | Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems[END_REF]. Like a veriT proof, a TSTP proof consists of a list of inferences. TSTP does not mandate any inference system; the meaning of the rules and the granularity of inferences vary across systems. For example, the E prover [START_REF] Schulz | System description: E 1.8[END_REF] combines clausification, skolemization, and variable renaming into a single inference, whereas Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF] appears to cleanly separate preprocessing transformations. SPASS's [START_REF] Weidenbach | SPASS version 3.5[END_REF] custom proof format does not record preprocessing steps; reverse engineering is necessary to make sense of its output, and optimizations ought to be disabled [START_REF] Blanchette | Semi-intelligible Isar proofs from machine-generated proofs[END_REF]Sect. 7.3].

Most SMT solvers can parse the SMT-LIB [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF] format, but each solver has its own output syntax. Z3's proofs can be quite detailed [START_REF] De Moura | Proofs and refutations, and Z3[END_REF], but rewriting steps often combine many rewrites rules. CVC4's format is an instance of LF [START_REF] Harper | A framework for defining logics[END_REF] with Side Conditions (LFSC) [START_REF] Stump | Proof checking technology for satisfiability modulo theories[END_REF]; despite recent progress [START_REF] Hadarean | Fine grained SMT proofs for the theory of fixed-width bit-vectors[END_REF][START_REF] Katz | Lazy proofs for dpll(t)-based SMT solvers[END_REF], neither skolemization nor quantifier instantiation are currently recorded in the proofs. Proof production in Fx7 [START_REF] Moskal | Rocket-fast proof checking for SMT solvers[END_REF] is based on an inference system whose formula processing fragment is subsumed by ours; for example, skolemization is more ad hoc, and there is no explicit support for rewriting.

Proof assistants for dependent type theory, including Agda, Coq, Lean, and Matita, provide very precise proof terms that can be checked by relatively simple checkers, meeting De Bruijn's criterion [START_REF] Barendregt | The challenge of computer mathematics[END_REF]. Exploiting the Curry-Howard correspondence, a proof term is a λ-term whose type is the proposition it proves; for example, the term λx. x, of type A → A, is a proof that A implies A. Proof terms have also been implemented in Isabelle [START_REF] Berghofer | Proof terms for simply typed higher order logic[END_REF], but they slow down the system considerably and are normally disabled. Frameworks such as LF, LFSC, and Dedukti [START_REF] Cousineau | Embedding pure type systems in the lambda-Pi-calculus modulo[END_REF] provide a way to specify inference systems and proof checkers based on proof terms. Our encoding into λ-terms is vaguely reminiscent of LF. The encoded rules also bear a superficial resemblance to deep inference [START_REF] Guglielmi | A system of interaction and structure[END_REF].

Isabelle and the proof assistants from the HOL family (HOL4, HOL Light, HOL Zero, and ProofPower-HOL) are based on the LCF architecture [START_REF] Gordon | Edinburgh LCF: A Mechanised Logic of Computation[END_REF]. Theorems are represented by an abstract data type. A small set of primitive inferences derives new theorems from existing ones. This architecture is also the inspiration behind automatic systems such as Psyche [START_REF] Graham-Lengrand | Psyche: A proof-search engine based on sequent calculus with an LCF-style architecture[END_REF]. In Cambridge LCF, Paulson introduced an idiom, conversions, for expressing rewriting strategies [START_REF] Paulson | A higher-order implementation of rewriting[END_REF]. A conversion is an ML function from terms t to theorems of the form t u. Basic conversions perform β-reduction and other simple rewriting. Higherorder functions combine conversions. Paulson's conversion library culminates with a function that replaces Edinburgh LCF's monolithic simplifier. Conversions are still in use today in Isabelle and the HOL systems. They allow a style of programming that focuses on the terms to rewrite-the proofs arise as a side effect. Our framework is related, but we trade programmability for efficiency on very large problems. Remarkably, both Paulson's conversions and our framework emerged as replacements for earlier monolithic systems.

Over the years, there have been many attempts at integrating automatic provers into proof assistants. To reach the highest standards of trustworthiness, some of these bridges translate the proofs found by the automatic provers so that they can be checked by the proof assistant. The TRAMP subsystem of ΩMEGA is one of the finest examples [START_REF] Meier | TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level (system description)[END_REF]. For integrating superposition provers with Coq, De Nivelle studied how to build efficient proof terms for clausification and skolemization [START_REF] De Nivelle | Extraction of proofs from the clausal normal form transformation[END_REF]. For SMT, the main integrations with proof reconstruction are CVC Lite in HOL Light [START_REF] Mclaughlin | Cooperating theorem provers: A case study combining HOL-Light and CVC Lite[END_REF], haRVey (veriT's predecessor) in Isabelle/HOL [START_REF] Fontaine | Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants[END_REF], Z3 in HOL4 and Isabelle/HOL [START_REF] Böhme | Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL[END_REF][START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF], veriT in Coq [START_REF] Armand | A modular integration of SAT/SMT solvers to Coq through proof witnesses[END_REF], and CVC4 in Coq [START_REF] Ekici | Extending SMTCoq, a certified checker for SMT (extended abstract)[END_REF]. Some of these simulate the proofs in the proof assistant using dedicated tactics, in the style of our simple checker for Isabelle (Sect. 6.1). Others employ reflection, a technique whereby the proof checker is specified in the proof assistant's formalism and proved correct; in systems based on dependent type theory, this can help keep proof terms to a manageable size. A third approach is to translate the SMT output into a proof text that can be inserted in the user's formalization; Isabelle/HOL supports veriT and Z3 in this way [START_REF] Blanchette | Semi-intelligible Isar proofs from machine-generated proofs[END_REF].

Proof assistants are not the only programs used to check machine-generated proofs. Otterfier invokes the Otter prover to check TSTP proofs from various sources [START_REF] Zimmer | Integrated proof transformation services[END_REF]. GAPT imports proofs generated by resolution provers with clausifiers to a sequent calculus and uses other provers and solvers to transform the proofs [START_REF] Ebner | System description: GAPT 2.0[END_REF][START_REF] Hetzl | Understanding resolution proofs through Herbrand's theorem[END_REF]. Dedukti's λΠ-calculus modulo [START_REF] Cousineau | Embedding pure type systems in the lambda-Pi-calculus modulo[END_REF] has been used to encode resolution and superposition proofs [START_REF] Burel | A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo[END_REF], among others. λProlog provides a general proof-checking framework that allows nondeterminism, enabling flexible combinations of proof search and proof checking [START_REF] Miller | Proof checking and logic programming[END_REF].

Conclusion

We presented a framework to represent and generate proofs of formula processing and its implementation in veriT and Isabelle/HOL. The framework centralizes the delicate issue of manipulating bound variables and substitutions soundly and efficiently, and it is flexible enough to accommodate many interesting transformations. Although it was implemented in an SMT solver, there appears to be no intrinsic limitation that would prevent its use in other kinds of first-order, or even higher-order, automatic provers. The framework covers many preprocessing techniques and can be part of a larger toolbox.

Detailed proofs have been a defining feature of veriT for many years now. It now produces more detailed justifications than ever, but there are still some global transformations for which the proofs are nonexistent or leave much to be desired. In particular, supporting rewriting based on global assumptions would be essential for proof-producing inprocessing, and symmetry breaking would be interesting in its own right.

Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Experiments presented in this report were carried out using the Grid'5000 testbed (https://www. grid5000.fr/), supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and several universities as well as other organizations. A mirror of all the software and evaluation data described in this paper is hosted by Zenodo. 4

  (Sko_All :conclusion ((∀x. p(x)) p(εx. ¬ p(x))) :args (x → (εx. ¬ p(x))) :subproof ((.c1 (Refl :conclusion (x (εx. ¬ p(x))))) (.c2 (Cong :clauses (.c1) :conclusion (p(x) p(εx. ¬ p(x)))))))) (.c3 (Cong :clauses (.c0) :conclusion ((¬ ∀x. p(x)) ¬ p(εx. ¬ p(x)))))

  u], motivating the suggestive brackets around L's and R's term argument. Lemma 2. Let xn be the variables fixed by Γ in order of occurrence. Then L(Γ)[t] = αβ λx 1 . . . . λx n . Γ(t) . By the induction hypothesis, the encoded antecedent is derivable. Thus, by the encoded BIND rule, the encoded succedent is derivable. CASES CONG, SKO ∃ , AND SKO ∀ : Similar to BIND. CASE TRANS: If Γ(t) = t, the substitution entries of Γ affect only variables that do not occur free in t. Hence, R(Γ)[t] = αβ L(Γ)[t], as required by the encoded TRANS rule. CASE LET: Similar to TRANS.

	Proof. By induction on Γ.

CASE ∅: L(∅)[t] = t = ∅(t) . CASE x, Γ: Let ȳn be the variables fixed by Γ. L(x, Γ)[t] = λx. L(Γ)[t] = αβ λx.λy 1 . . . . λy n . Γ(t) {by the induction hypothesis} = λx.λy 1 . . . . λy n . (x, Γ)(t) {by ( * )} where ( * ) is the property that subst(Γ) = subst(x, Γ) for all x and Γ, which is easy to prove by structural induction on Γ. CASE xn → sn , Γ: Let ȳn be the variables fixed by Γ, and let ρ = { xn → sn }[ȳ n → ȳn ]. L( xn → sn , Γ)[t] = (λ xn . L(Γ)[t]) sn = αβ (λ xn .λy 1 . . . . λy n . Γ(t) ) sn {by the induction hypothesis} = αβ λy 1 . . . . λy n . ρ(Γ(t)) {by β-reduction} = λy 1 . . . . λy n . ( xn → sn , Γ)(t) {by ( * * )} where ( * * ) is the property that ρ • subst(Γ) = subst( xn → sn , Γ) for all xn , sn , and Γ, which is easy to prove by structural induction on Γ. Lemma 3. If the judgment Γ t u is derivable using the original inference system, then L(Γ)[t] R(Γ)[u] is derivable using the encoded inference system. Proof. By structural induction on the derivation of Γ t u. CASE TAUT T : We have |= T Γ(t) u. Using Lemma 2, we can easily show that |= T Γ(t) u is equivalent to |= T reify(L(Γ)[t] R(Γ)[u]), the side condition of the encoded TAUT T rule. CASE BIND: The encoded antecedent is M[λy. (λx. ϕ) y] N[λy. ψ] (i.e., L(Γ, y, x → y) [ϕ] R(Γ, y, x → y)[ψ]), and the encoded succedent is M[Qx. ϕ] N[Qy. ψ].

the judgment expresses the equality of the terms Γ(t) and u for all variables fixed by Γ. Crucially, the substitution applies only on the left-hand side of the equality.The inference rules for the transformations covered in this report are presented below, followed by explanations.TAUT T if |= T Γ(t) u Γ t u

http://isabelle.in.tum.de/repos/isabelle/file/00731700e54f/src/HOL/ex/veriT _ Preprocessing.thy

http://matryoshka.gforge.inria.fr/pubs/processing/veriT.tar.gz

http://matryoshka.gforge.inria.fr/pubs/processing/

https://doi.org/10.5281/zenodo.582482

Acknowledgment We thank Simon Cruanes for discussing many aspects of the framework with us as it was emerging, and we thank Robert Lewis, Stephan Merz, Lawrence Paulson, Anders Schlichtkrull, Mark Summerfield, Sophie Tourret, and the CADE-26 anonymous reviewers for suggesting many textual improvements. This research has been partially supported by the Agence nationale de la recherche / Deutsche Forschungsgemeinschaft project SMArT (ANR-13-IS02-0001, STU 483/2-1) and by the European Union project SC 2 (grant agreement No. 712689). The work has also received funding from the European Research Council under the European Union's