A Guide to Seduct

Release 1.3

Karl Stroetmann in collaboration with Claus Bendix Nielsen

Siemens AG Corporate R & D Confidential Report

February 24, 1994

Abstract

This guide provides an introduction to Seduct, Release 1.3 of July 1993. It describes how Seduct can be used to prove theorems in a many–sorted first-order logic. It is further shown how this feature can be utilized to prove the correctness of abstract algorithms. Furthermore, this manual contains a tutorial overview of the sequent calculus and the term rewriting technology that makes up, along with induction rules, the inference engine of Seduct.

Seduct is designed primarily as a “proof compiler” rather than as an automatic theorem prover or as an interactive theorem prover. It accepts so called abstract proofs of theorems as inputs and compiles these abstract proofs into machine checked mathematical proofs. For us, an abstract proof is a high–level sketch of a proof, i.e., it contains the main structure of a proof. This main structure consists of the lemmata needed during the proof together with information concerning the method by which each lemma can be proved, i.e., if it is simply a first order consequence of certain axioms, or if induction has to be applied in order to prove it.

Contents

1 Introduction 6 1.1 Structure of the Manual . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2 Getting Started 8 2.1 Starting Seduct and Entering Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 A First Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 The Command Language of SEDUCT 12 3.1 Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.2 The Syntax of Terms and Formulae . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.3 The Structure of Command Files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3.3.1 The declare section . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.3.2 The operator section . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3.3 The axioms section . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.3.4 The definitions section . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3.5 The goals section . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.3.6 The theories section . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.3.7 The proofs section . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4 Verification of Algorithms with SEDUCT 31

4.1 Verification of the Insertion Sort Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.2 Verification of the Correctness of the Quicksort Algorithm . . . . . . . . . . . . . . . . . . . . . . . 37

4.2.1 The Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 4.2.2 The Proof Development . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 4.2.3 Presenting the Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

5 The Sequent Calculus 50 5.1 What Constitutes a Formal Proof? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 5.2 A Cut Free Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 5.3 The Preprocessing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 5.4 The Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 5.5 The α Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 5.6 The β Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 5.7 The γ Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 5.8 The δ Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 5.9 Additional Rules for Dealing with Quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 5.10 The ι Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 5.11 An Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

6 The Rewriting Techniques Employed by SEDUCT 62 6.1 Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 6.2 The Rewrite Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 6.3 The Axioms of the Rewrite Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 6.4 Rules Changing the Antecedent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 6.5 Rules Changing the Succedent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 6.6 The Control Strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 6.7 An Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

7 Commands Available in SEDUCT 72 7.1 Command Interpreter Modes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 7.2 Short-hands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 7.3 Commands Available in Seduct in Any Mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

7.3.1 arity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 7.3.2 associative commutative . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 7.3.3 associative commutative idempotent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 7.3.4 axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 7.3.5 begin( axioms ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 7.3.6 begin( believe ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 7.3.7 begin( declare ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 7.3.8 begin( definitions ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 7.3.9 begin( goals ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 7.3.10 begin( operators ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 7.3.11 begin( theories ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 7.3.12 begin( time ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 7.3.13 clear . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 7.3.14 close . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 7.3.15 definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 7.3.16 disjoint . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 7.3.17 do not show proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 7.3.18 end( believe ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 7.3.19 end( time ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 7.3.20 end . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 7.3.21 end of file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 7.3.22 execute . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 7.3.23 exit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 7.3.24 freely generated . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 7.3.25 generated . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 7.3.26 goal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 7.3.27 help . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 7.3.28 inform . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 7.3.29 injective . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 7.3.30 instantiate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 7.3.31 linear ordered . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 7.3.32 macro . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 7.3.33 monotone . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 7.3.34 op . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 7.3.35 operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 7.3.36 protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 7.3.37 prove . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 7.3.38 quit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 7.3.39 remove . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 7.3.40 rewrite counter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 7.3.41 run . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 7.3.42 set( show ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 7.3.43 set( strict ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 7.3.44 show . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 7.3.45 show proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 7.3.46 system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 7.3.47 theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 7.3.48 unset( show ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 7.3.49 unset( strict ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

7.4 Commands Available in the Prove Mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 7.4.1 abort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 7.4.2 add . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 7.4.3 alpha normalize . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 7.4.4 believe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 7.4.5 beta normalize . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 7.4.6 case induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 7.4.7 cases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 7.4.8 crunch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 7.4.9 cut . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 7.4.10 expand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 7.4.11 expand all . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 7.4.12 go . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 7.4.13 induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 7.4.14 instantiate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 7.4.15 instantiate forall . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 7.4.16 instantiate exists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 7.4.17 lazy induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 7.4.18 select . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 7.4.19 select shadow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 7.4.20 show . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 7.4.21 skolemize . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 7.4.22 split if . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 7.4.23 use as definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 7.4.24 unfold . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102

A The Syntax of SEDUCT 103

A.1 The Scanner . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 A.1.1 Letters, Digits, and Underscore . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 A.1.2 Special Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 A.1.3 Forbidden Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 A.1.4 Separator Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 A.1.5 Operator symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 A.1.6 Tokens Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105

A.2 The Parser . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

1 Introduction

Seduct is a proof development system for many–sorted first–order logic. Seduct has efficient methods for dealing with

• equalities,

• inequalities and

• freeness axioms.

It is designed to work economically on large problems and to be used by users having little or no previous experience with formal methods. It is intended to be used in a software verification environment together with tools generating first order verification conditions. It is already used for verifying proof obligations generated by the KIV–system.^{1} Furthermore, Seduct is used as a theorem prover for verifying proof obligations generated by CCC. ^{2}

Seduct is primarily used as an interactive proof assistant, not as a fully automatic theorem prover. Its design is based on the experience that, unless one is trying to reproduce well known results from textbooks, initial attempts to state conjectures correctly, and then to prove them, usually fail. As a result, Seduct is designed to carry out routine (and possibly lengthy) steps in a proof automatically and to provide useful information about why proofs fail, if and when they do. Therefore Seduct usually fails quickly if it fails at all. On the negative side, this implies that Seduct will also fail in those cases, where a proof exists but is quite complicated. However, by changing certain switches, the user has the possibility to change this feature to a certain extent.

Seduct can also be seen as a proof compiler. Using Seduct as a proof compiler works as follows. When starting to prove a conjecture, a sketch of the proof is developed with pencil and paper. This proof sketch will already contain the main lemmata needed in order to carry through the proof. We call this sketch of a proof an “abstract proofindexabstract proof”. This abstract proof is then formalized. At this stage of the proof each lemma has to be annotated with a proof method, i.e., it has to be specified whether the lemma follows logically from other lemmata already proven or whether induction has to be applied in order to carry its proof through. If the abstract proof is given in this way, and is furthermore correct, Seduct will be able to compile this proof and thereby verify its correctness. If the proof is either not correct or not complete Seduct will help to spot the problems with this proof. It will give useful hints to the user to enable him to correct either the proof or the theorem he wanted to prove.

To ensure that users will not lose track of what is going on, Seduct does not employ lots of complicated heuristics for finding proofs automatically. Rather, Seduct has implemented one powerful method for proof search which will be sufficient in most cases. Since this method is quite straightforward, it will be possible for the user to understand what is happening if the search for a proof fails. Additionally, Seduct makes it easy for the user to employ standard proof techniques like proof by induction or proof by cases.

Finally, a word of warning is in order. With the current state of the art we simply cannot expect theorem provers to find proofs of complicated mathematical conjectures automatically. There might be a few, happy coincidences where an interesting, new theorem can be proved by an automated theorem prover. However, at least in the near future, this will always be the exception rather than the rule. Nevertheless, it is reasonable to expect a theorem prover to do the proof of a complicated theorem after being given a number of hints. This is the main idea behind the design of Seduct. If you read a textbook in mathematics you will not find every proof spelled out in minute detail. Rather, you will find something like “… the proof is done by an easy induction on n. In the induction step you have to perform a side induction on m …” which gives you an outline along which you could, in principle, develop a formal proof. Now the idea behind Seduct is this: To prove a complicated theorem with the help of Seduct you have to specify an outline of the proof, or, as we prefer to call it, an abstract proof. The task of Seduct then is to fill in the formal details of this abstract proof, thereby verifying that the abstract proof (and therefore also the theorem) is correct.

1KIV is short for \underline{K}arlsruhe \underline{I}nteractive \underline{V}erifier. The KIV–system [7] is a tool to develop correct programs. It works mainly as a tactical theorem prover for dynamic logic.

2CCC is short for \underline{C}onsistency and \underline{C}ompleteness \underline{C}hecker. CCC is a tool for producing correct Prolog programs.

1.1 Structure of the Manual

This Manual is structured as follows. In the next Section we will explain how to start Seduct and we will furthermore give a small example illustrating some of the basic features of Seduct. Section 3 will give an overview over the syntax of commands, while Section 4 contains a tutorial illustrating the proof of the correctness of some sorting algorithms with Seduct. Section 5 is an introduction to the sequent calculus embodied in Seduct, while Section 6 focuses on the rewrite techniques. Section 5 and 6 are rather theoretical and can be skipped on a first reading. Finally, Section 7 contains a description of all commands available. It is primarily intended as a reference guide.

1.2 Acknowledgements

Although Seduct started as a one man show, in the meantime it has benefited from several contributions. First of all, Seduct is based on a rewriting tool which had notable contributions from Dr. Peter Warkentin and Gerd Gouverneur. The algorithms concerning unification have been implemented by Hans–Albert Schneider in C++. Sabine Glesner started to implement the component handling faulty user inputs and thereby ensured some form of robustness of the program. Dr. Peter Päppinghaus spotted a number of errors and made some useful suggestions during the time when he integrated certain features of Seduct into his system Sinda.

2 Getting Started

This section describes how to use elementary Seduct features for entering commands and displaying information.

2.1 Starting Seduct and Entering Commands

Working with Seduct requires the definition of a number of environment variables. In order not to bother the user of Seduct with unnecessary details we have written a shell script which performs these definitions and afterwards starts Seduct. It is most convenient to run this script via an alias. Therefore our recommendation is to add the following line to the end of the .cshrc file in your home directory (assuming Seduct has been

installed in /home/gentzen/prover/SEDUCT):
      alias seduct /home/gentzen/prover/SEDUCT/seduct

Since Seduct is built on top of SNI–Prolog you have to be in possession of a valid licence for SNI–Prolog to use Seduct.

To be able to work properly with Seduct you must have read and write access to the current directory. (The write access is needed because Seduct creates a script file named script to protocol your session.) To start working with Seduct you can simply type

      seduct

in response to the prompt of your shell. After that, three things should happen:

• The SNI–Prolog system is loaded.

• Seduct is loaded into the Prolog system.

• Seduct is started.

During loading of the system the following messages will appear on your screen:

      SNI-PROLOG Development System Version 3.0A created 17/5/93
      Copyright (c) 1990-92 Siemens Nixdorf Informationssysteme AG
      Serial 2-301100018 licensed for X2000 (ZFE BT SE 11)
      Welcome to SEDUCT, Release 1.3 (July 1993).
      Copyright (C) 1992, 1993  Siemens AG (ZFE BT SE 11).
      SEDUCT>

(Do not bother if the message is not exactly the same as above. The shell variable PROROOT specifying where the Prolog system is to be found as well as the version number are subject to constant changes.) Seduct generally prompts users to enter commands interactively from the keyboard. The prompt takes either of the following forms: It is

       SEDUCT>

if the user is not proving a theorem, otherwise it takes the form

       SEDUCT(goal):

where goal is the name of the theorem currently being proved.

Users can also create files containing sequences of commands and instruct Seduct to execute these command files; for example the command^{3}

3Notice that the prompt SEDUCT> is not part of the command to be executed.

       SEDUCT> execute(first.sed).

causes Seduct to execute the commands in the file “first.sed”. (Of course, for this to work there has to be a command file named “first.sed” in your current directory.) Execution of a command file continues until the command file is exhausted, until an error occurs or until a quit or exit command is executed. To exit from Seduct you type

       SEDUCT> exit.

followed by a carriage return. This will end the Seduct session.

You may have already noticed that all legal commands for Seduct are written as Prolog terms and are followed by a dot “.”. Furthermore, commands have to be separated by at least one whitespace character.^{4} (The reason all commands have to be written as Prolog terms is that Seduct is implemented in Prolog and uses the Prolog parser to read its input.)

When Seduct gets stuck, in most cases the key “Control-C” will help us out and abort any nonterminating loop. If this fail, then there is always the possibility of using “Control-\”. This will kill Seduct, but it will also produces a core dump which should be removed afterwards.

2.2 A First Example

By now you are probably eager to try it out for yourself, so we will start with a first small example. We have taken this example from group theory, not because we think that this is a particularly interesting theory, but because we think it is quite well known and easy for a beginning. Group theory is made up of the following three axioms:

1. ∀x, y, z( (x ∗ y) ∗ z = x ∗ (y ∗ z) ) (Associativity)

2. ∀x( 1 ∗ x = x ) (Left Neutral)

3. ∀x( x^{−1} ∗ x = 1 ) (Left Inverse)

We want to show that the left inverse inv(x) is also a right inverse:

∀x( x ∗ x^{−1} = 1 )

To start with, we have to define the signature, i.e., we have to declare symbols representing the constant 1 and the functions x ↦ x^{−1} and ⟨x, y⟩ ↦ x ∗ y. Declaring these symbols is achieved via the commands:

       SEDUCT> arity( 1:  gr ).
       SEDUCT> arity( inv:  [ gr ] -> gr ).
       SEDUCT> arity( times:  [ gr, gr ] -> gr ).

These commands will define 1 as a constant of sort gr, the symbol inv is defined to denote a unary function mapping elements of sort gr to elements of sort gr, while times is declared as a binary function mapping a pair of elements each of sort gr to an element of sort gr. Our intention is, of course, that inv will be a name for the function x ↦ x^{−1} while times represents the function ⟨x, y⟩ ↦ x ∗ y. It is convenient to use the function symbol times as an infix operator. This can be achieved via the command

       SEDUCT> op( 100, xfx, times ).

The syntax and semantics of the op command in Seduct is the same as in Prolog. It will be fully explained in Section 7.

To proceed we have to enter the axioms of our theory. This is done as follows:

       SEDUCT> axiom( a1:  forall( [x:  gr, y:  gr, z:  gr],
                           (x times y) times z = x times (y times z) ) ).
       SEDUCT> axiom( a2:  forall( x:  gr, 1 times x = x ) ).

4Whitespace characters are, among others, blanks, tabulators, and newlines.

       SEDUCT> axiom( a3:  forall( x:  gr, inv(x) times x = 1 ) ).

Next, we specify the goal we are going to prove. This is done via:

       SEDUCT> goal( g:  forall( x:  gr, x times inv(x) = 1 ) ).

Now we are ready to start the proof. This is done via the command

       SEDUCT> prove( g, [ a1, a2, a3 ] ).

It tells Seduct to prove the goal named g from the axioms named a1, a2 and a3. After entering the prove command, Seduct will display the message

       % Now proving:  "g".

and furthermore the prompt of Seduct will change to

       SEDUCT(g):

informing us that we are currently trying to prove a goal named g. The proof can now be carried out by typing “go.” in response to this prompt, i.e., the command line has to be

       SEDUCT(g):  go.

After a short time Seduct will display the message

          % Proof of "g" finished.

and the prompt will change back to

       SEDUCT>

This will inform us that Seduct has successfully finished the proof of the goal “g” and is now waiting for further input. In order to convince ourselves that the proof has really taken place, we issue the command

       SEDUCT> show( theorems ).

Seduct will respond to this command by displaying

       g :  forall(x :  gr,x times inv(x) = 1)

ensuring us that the former goal g has been converted into a theorem.

The example above illustrates a number of points. It begins with declarations. Every constant, every function symbol and every predicate symbol being used has to be declared. Generally, you can use an arbitrary Prolog atom^{5} as a designator of a constant, function or predicate. Because Seduct implements a many–sorted predicate logic we have to specify the sort of every constant. To declare c as a constant of sort s the command

       arity( c:  [] -> s ).

can be used. There is also a short hand notation for the declaration of constants. It is

       arity( c: s ).

To declare f as a symbol denoting a function with domain the cartesian product s_{1} × ⋯ × s_{n} and range the sort s, the following command is used:

       arity( f:  [ s_{1}, · · ·, s_{n} ] -> s ).

In the last command neither the dots nor the index _{n} is to be taken literally. To declare p to denote a predicate defined on the cartesian product s_{1} × ⋯ × s_{n}, the following command is used:

       arity( f:  [ s_{1}, · · ·, s_{n} ] -> bool ).

Syntactically, the declaration of a predicate is just a special case of the declaration of a function symbol. This is because we regard predicates as Boolean valued functions. Furthermore, the symbol bool denotes a reserved sort which is equipped with the constants true and false. The sort bool is subject to some restrictions: For example, you are not allowed to include the sort bool in the domain of a function or a predicate. Also the range of a function is not allowed to be the sort bool. Otherwise it would not be possible to distinguish between function declarations and predicate declarations.

5Of course, there are some restrictions. Atoms used for constants or function symbols may neither start with the letter c followed by a natural number nor may they start with the letter s followed by a natural number. The reason for these restrictions is that Seduct uses symbols of this kind to denote Skolem constants.

Returning to our example we note that the declaration of the syntactic material was followed by the declaration of the axioms. The general form of an axiom is

axiom( Name: Formula ). where Name is a unique name and Formula is the formula which is to be asserted as axiom. The syntax of formulae will be described in the next section.

The specification of a goal looks very similar to the specification of axioms. To declare the formula Goal as a goal to be proved we have to enter the command

goal( Name: Goal ). where, again, Name is a unique name referring to this goal.

After having entered the axioms and goals we are ready to start proving a goal. Entering

prove( Name, Theory ). requests Seduct to prove the goal referred to by Name. Here Theory stands for a collection of axioms and goals which have already been proved. Usually Theory will be a list of names referring either to those axioms or theorems, which are to be used in the proof of the goal referred to by Name. After reading this command Seduct will change its prompt to

       SEDUCT(Name):

informing the user that the proof of the goal referred to by Name has started. To get Seduct working on this task we can issue the “go” command:

       go.

which starts the automatic theorem prover embedded in Seduct. If the proof is successful the user is informed that the goal has been proved and the prompt changes back to

       SEDUCT>

while Seduct is waiting for the next task to be proved. However, the go command will only work when the goal to be proved is a first order consequence of the axioms. In particular the proof will fail if it requires an inductive argument. If the proof should fail, Seduct will inform the user of this fact via printing

       % Proof suspended.

In this case the prompt will not change. The user can now type

     SEDUCT(g1): abort.

if he wants to abort this particular proof attempt or he might try to proceed with a proof by induction, a proof by cases or any other of the special methods implemented in Seduct. These will be described in the next section.

3 The Command Language of SEDUCT

This section gives a survey of the syntax of the command language of Seduct. We start with the specification of some typesetting conventions.

• In this manual Seduct command names and other keywords are printed in typewriter type style (e.g.,

      prove, induction, go, cases).

• Syntactical variables are printed in boldface (e.g., c, f, p, S, T). If a syntactical variable refers to a complex object like a term or formula, it will start with a capital letter (e.g., T, F), if it refers to a symbol, lower case letters will be used. Note that a syntactical variable is not an object of the input language of Seduct, but rather an object of our meta language denoting an object of the Seduct language.

• Mathematical and logical notions, like the set of variables free in a formula F, will be written in math style (e.g., F V (F)).

Furthermore, we have to define a lot of basic objects from which command files can be built. To ease this burden we will always apply the following convention: Any class of syntactic objects not explicitly defined in this manual is taken to consist of the set of all Prolog atoms. For example, we will not define sorts, constant symbols, function symbols or predicate symbols. Therefore syntactically these are all Prolog atoms.^{6} Since Prolog atoms may not start with an uppercase letter, we are not permitted to use names starting with an uppercase letter in Seduct commands.

There is one other convention, or rather an abuse of the standard terminology, that we will constantly apply from here on: Rather than speaking of, for example, a function symbol f we will just speak of a function f. Taken literally this would not be correct because f is a meta variable standing for a function symbol, for example the string square, which in turn denotes the function x ↦ x^{2} mapping every natural number n to n^{2}. In future, these subtleties will not bother us any more.

Next, we define the syntax of declarations.

3.1 Declarations

Every constant, every function and every predicate has to be declared prior to its use. If c is used as a constant of sort s, its declaration has the form:

c: s For example, if we want to use the string “zero” as a constant referring to a natural number, where the sort of natural numbers is written as nat, then we will use a declaration like the following:

      zero: nat

A function f defined on the cartesian product s_{1} × ⋯ ×s_{n} and producing values of sort s will be declared as:

f:[ s_{1}, ⋯, s_{n} ] -> s As an example take a function insert taking one element of sort nat and one element of type list and producing an element of sort list. It would be declared as:

      insert: [ nat, list ]  ->  list

6The set of all Prolog atoms is the set of all those strings which consist solely of

1. the lower case letters a, b, c, …, x, y, z,

2. the upper case letters A, B, C, …, X, Y, Z,

3. the digits 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,

4. and the underscore character “ ”;

5. and which furthermore start with a lower case letter.

Defining a predicate p with domain the cartesian product s_{1} × ⋯ ×s_{n} is achieved by:

       p:[ s_{1}, · · ·, s_{n} ] -> bool

To give an example, imagine a predicate same length taking as arguments two lists (and returning true if they have the same length). This could be declared as:

      same_length: [ list, list ]  ->  bool

Now we are able to define the syntax of terms and formulae.

3.2 The Syntax of Terms and Formulae

Due to the presence of the “if” operator terms and formulae have to be defined via a simultaneous induction. We start with the definition of the notion “T is a term of sort s”. Together with the terms we define the notions FV (T) and BV (T) as the set of free and bound variables of the term T respectively.

1. If x is a variable, then x is a term of sort s for any sort s with FV (x) = {x} and BV (x) = ∅.

2. If c is a constant of sort s, i.e., if c is declared via

c: s, then c is a term of sort s with

FV (c) = BV (c) = ∅.

3. If f is a function declared as

f:[ s_{1}, ⋯, s_{n} ] -> s, and if, furthermore, T_{1}, ⋯, T_{n} are terms of sort s_{1}, ⋯, s_{n} respectively, then f(T_{1}, ⋯, T_{n}) is a term of sort s with

FV (f(T_{1}, ⋯, T_{n})) = FV (T_{1}) ∪ ⋯ ∪ FV (T_{n}) and

BV (f(T_{1}, ⋯, T_{n})) = BV (T_{1}) ∪ ⋯ ∪ BV (T_{n}).

4. If S and T are terms of sort s and F is a formula, then

             if( F, S, T )

is a term of sort s with FV ( if( F, S, T ) ) = FV (F) ∪ FV (S) ∪ FV (T) and

BV ( if( F, S, T ) ) = BV (F) ∪ BV (S) ∪ BV (T) .

This definition is subject to the additional restriction that a variable x may only be used as a variable for one sort, i.e., we may not use x both as a variable of sort s_{1} and as a variable of sort s_{2} in the same term when s_{1} is different from s_{2}.

To illustrate this definition, we give some examples of terms. Suppose the following declarations have been given:

      zero:  nat.
      succ:  [ nat ]  ->  nat.
      empty: list.
      cons:  [ nat, list ]  ->  list.

Then the following strings are terms:

    x,  y,  l,   zero,  empty,   succ(x),  cons(zero,cons(succ(x),l))

Here x, y and l have to be variables since they are not declared as constants. However,

       cons(x,x)

is not a term because it violates the restriction that a variable may only have one sort. For cons(x,x) to be a term, the first occurrence of x would have to be a variable of sort nat, while the second occurrence would have to be a variable of sort list. Furthermore, even if F is a formula, the string

       if( F, zero, empty )

is not a term since zero is a term of sort nat while empty is a term of sort list and the sort nat is different from the sort list, simply because the strings “nat” and “list” are not literally identical.

Finally, we should note that function and predicate symbols may be used as infix, prefix or postfix operators. This is possible if they are either predefined operators of the appropriate type or else have been declared as such via the “op” command, which is explained in section 7. A complete list of all predefined operators can also be found in Section 7. In this section it will be sufficient for us to note that the usual arithmetical operators (“+”, “-”, “*”, and “/” ) may be used as infix operators. Therefore also

    x + (y + z),  x * y - (x + y) / (x - y)

are legal terms^{7}, provided the operators involved have been declared as binary functions.

The definition of terms is not yet complete since we have not yet defined the notion of a formula. This is done next.

0. The strings true and false are formulae with FV (true) = FV (false) = BV (true) = BV (false) = ∅.

1. If S and T are terms of the same sort, then the strings

             S = T, S < T, S > T, S =< T, S >= T

are formulae. If F is any of the above formulae, we define the sets of free and bound variables as FV (F) = FV (S) ∪ FV (T) and BV (F) = BV (S) ∪ BV (T).

2. If p is a predicate declared as

             p:[ s_{1}, · · ·, s_{n} ]  ->  bool,

and if, furthermore, T_{1}, ⋯, T_{n} are terms of sort s_{1}, ⋯, s_{n} respectively, then p(T_{1}, ⋯, T_{n}) is a formula. The free and bound variables of this formula are defined as

FV (p(T_{1}, ⋯, T_{n})) = FV (T_{1}) ∪ ⋯ ∪ FV (T_{n}) and

BV (p(T_{1}, ⋯, T_{n})) = BV (T_{1}) ∪ ⋯ ∪ BV (T_{n}).

3. If F is a formula, then (F) is a formula with the same free and bound variables as F.

4. If B, F and G are formulae, then the following are formulae:

• ^F with FV (^F) = FV (F) and BV (^F) = BV (F).

• F & G with FV (F & G) = FV (F) ∪ FV (G) and BV (F & G) = BV (F) ∪ BV (G).

• F v G with FV (F v G) = FV (F) ∪ FV (G) and BV (F v G) = BV (F) ∪ BV (G).

• F -> G with FV (F -> G) = FV (F) ∪ FV (G) and BV (F -> G) = BV (F) ∪ BV (G).

• F <--> G with FV (F <--> G) = FV (F) ∪ FV (G) and BV (F <--> G) = BV (F) ∪ BV (G).

• if( B, F, G ) with FV (if( B, F, G )) = FV (B) ∪ FV (F) ∪ FV (G) and

BV (if( B, F, G )) = BV (B) ∪ BV (F) ∪ BV (G).

7Note that one has to use parentheses to disambiguate between different interpretations.

Meaning is given to these formulae by interpreting “^” as negation, “&” as conjunction, “v” as disjunction, “->” as implication, “<-->” as equivalence and “if( B, F, G ) ” as “(B -> F) & (^B -> G)”. For a deeper discussion of semantics the reader is referred to textbooks on mathematical logic like Enderton [4].

5. If x is a variable and F is a formula, such that

(a) x ∉ BV (F) and

(b) x is only used as a term of sort s in F,

then the string forall( x: s, F ) is a formula. The free and bound variables of this formula are defined respectively as

FV ( forall(x:s,F) ) = FV (F) − {x} and BV ( forall(x:s,F) ) = BV (F) ∪ {x}. This formula is intended to be true if the formula F[x←c] holds regardless how the constant c, which has to be of sort s, is interpreted. (Here F[x←c] stands for the formula which results from F by replacing every occurrence of x by c.)

6. If x is a variable and F is a formula, such that

(a) x ∉ BV (F) and

(b) x is only used as a term of type s in F,

then the string exists( x: s, F ) is a formula. The free and bound variables of this formula are defined respectively as

FV ( exists(x:s,F) ) = FV (F) − {x} and BV ( exists(x:s,F) ) = BV (F) ∪ {x}. This formula is intended to be true if there is an interpretation for a constant c of sort s such that F[x←c] holds.

Any formula constructed according to the first or the second rule of this definition is called a prime formula. A literal is either a prime formula or a negated prime formula. We call a formula F closed, iff the set of free variables of F is empty:

F is closed ⟺^{def} FV (F) = ∅.

Any formula used as input for Seduct has to be closed.

Finally, we want to give some examples. Assuming the declaration

zero: nat.
succ: [ nat ]      ->  nat.
empty: list.
cons: [ nat, list ]  ->  list.
plus: [ nat, nat ]  ->  nat

the following is a formula (expressing the associativity of plus):

forall(x:nat, forall(y:nat, forall(z:nat, plus(plus(x,y),z) = plus(x,plus(y,z)) )))

Because the nesting of universal quantifiers is hard to read and therefore inconvenient, there is a shorthand available for expressing nested universal quantifiers. With this shorthand the formula above may be written as

forall( [ x: nat, y: nat, z: nat ], plus(plus(x,y),z) = plus(x,plus(y,z)) )

which is much more readable. Of course, the same shorthand is available for existentially quantified formulae.

The string

 forall( x:  nat, forall( l:  list, if( x = l, true, false ) ) )

is not a formula because the variables x and l would have to be of the same sort for the expression “if( x = l, true, false ) ” to be a formula, but the quantifiers define x to be of sort nat while l is of sort list. Another string that is not a formula is given by

       exists( x:  nat, forall( x:  nat, x = x ) ).

This is not a formula since x is a member of the set of bound variables of the formula

       forall( x:  nat, x = x ) )

and therefore the outermost existential quantification is not admitted.

Having the basic syntactic material at our disposal, we are able to describe the general structure of a command file.

3.3 The Structure of Command Files

Generally, a command file for Seduct consists of seven parts, some of which are optional:

1. The declare section contains the declarations of all constants, functions and predicates.

2. The operator section contains the definition of precedences for the operators defined in the declare section. These precedences are used for the comparison of terms during rewriting. The operator section is optional.

3. The axioms section consists of a collection of axioms from which theorems will be deduced.

4. The definitions section consists of a collection of definitions. Logically, definitions are equivalent to axioms. However, definitions are directed and can be expanded or unfolded.

5. The theories section contains the declaration of theories. A theory is a collection of axioms and theorems. The theories section is optional.

6. The goals section contains the goals which are going to be proved by Seduct.

7. The proofs section contains commands to guide the proofs of the goals.

These sections do not have to appear in the order they are listed here. Rather, they can be mixed in any order that makes sense, e.g., we can not start the prove of a goal before the goal has been defined. However, what can be done is the following: If we recognize during the proof of a goal that we need a further lemma not yet defined, we can interrupt the proof of the current goal and define a new goal, prove this new goal, and then continue with the original goal. We will now describe each of the sections mentioned above in more detail.

3.3.1 The declare section

The general form of a declare section is this:

       begin( declare ).

Declaration_{1}.

⋮

Declaration_{n}.

       end( declare ).

The declarations to be entered between “begin(declare)” and “end(declare)” come in three possible forms:

• A constant c of sort s is declared via:

c: s

• A function f with domain s_{1} × ⋯ ×s_{n} and range s will be declared as: f:[ s_{1}, ⋯, s_{n} ] -> s • A predicate p defined on the set s_{1} × ⋯ ×s_{n} is introduced via:

             p:[ s_{1}, · · ·, s_{n} ] -> bool

Instead of entering these declarations via a declare section, declarations can also be entered via a command of the form

arity( Declaration ). This command has the same effect as the following declare section:

       begin( declare ).

Declaration.

       end( declare ).

Finally, a typical declare section might look like follows:

    begin( declare ).  zero: nat.
        succ: [ nat ] -> nat.
        plus: [ nat, nat ] -> nat.
    end( declare ).

This would declare zero as constant of type nat, succ as function from nat to nat and plus as a function mapping a pair of nats into a nat.

3.3.2 The operator section

The operator section is used to define operator precedences for the operators, i.e., the constants, functions, and predicates defined earlier. Operator precedences provide a means for the more experienced user of Seduct to influence the way in which equations are ordered into rewrite rules. An equation l = r is turned into a rewrite rule l → r if r <_{lpo} l holds, where <_{lpo} is the \underline{l}exicographic \underline{p}ath \underline{o}rdering. If < is an ordering of the set of operator symbols, then the lexicographic path ordering is defined recursively as follows: Given that

s ≡ f(s_{1}, ⋯, s_{m}) and t ≡ g(t_{1}, ⋯, t_{n})

holds, we define s <_{lpo} t if and only if one of the following cases is satisfied:

1. s is a proper subterm^{8} of t.

2. f < g and for all i ∈ {1, ⋯, m} we must have s_{i} <_{lpo} t.

3. f = g and (s_{1}, ⋯, s_{m}) ≪_{lpo} (t_{1}, ⋯, t_{m}), where ≪_{lpo} is the lexicographic extension of the ordering <_{lpo} to tuples of terms.^{9}

Furthermore, for all i ∈ {1, ⋯, m} we have s_{i} <_{lpo} t.

4. f > g and there is an i ∈ {1, ⋯, n} such that s <_{lpo} t_{i}.

For a variable x and a term s we have x <_{lpo} s if and only if x is a proper subterm of s.

So in order to specify a lexicographic path ordering one has to specify an ordering on the operator symbols. This ordering is implemented in Seduct by assigning an integer to each predicate symbol, function symbol and constant which has been declared. Normally the assignment of integers to operators is done automatically. However, in the current version the way in which these integers are assigned is not necessarily optimal. Therefore there are situations where it is advisable to perform these assignments manually via the operator section. The form of an operator section is as follows:

8A subterm s is a proper subterm of t if and only if s is a subterm of t and furthermore s is different from t.

9If S is a set ordered by <, then for all n ∈ IN the set S^{n} of all n–tuples of elements of S is ordered lexicographically via the following definition:

(a_{1}, ⋯, a_{n}) ≪ (b_{1}, ⋯, b_{n}) iff

a_{1} < b_{1} or a_{1} = b_{1} and (a_{2}, ⋯, a_{n}) ≪ (b_{2}, ⋯, b_{n}).

       begin( operators ).

Op–Assignment_{1}.

⋮

Op–Assignment_{n}.

       end( operators ).

Alternatively, if we want to assign a precedence to just one operator, the syntax

operator( Op–Assignment ) . will be sufficient. The syntax of an Op–Assignment is given as

Op: n where n is a natural number. An operator assignment of this form has the effect of assigning the integer n to the operator Op, where Op denotes either a predicate, a function or a constant. Later on, if operator symbols have to be compared, this comparison is made according to the value of n. As an example, consider the following

operator section:
    begin( operators ).
           zero: 0.
           succ: 1.
           plus: 2.
    end( operators ).

This operator section would be sufficient to guarantee that the equations

       plus(x,zero) = x.
       plus(x,succ(y)) = succ(plus(x,y)).

are ordered from left to right.^{10} For example, the assignment above guarantees plus > succ. Therefore we have

       succ( plus(x,y) ) <_{lpo} plus( x, succ(y) )

To convince us of this inequalitity we first have to compare the leading function symbols of these terms, in our case succ and plus. Since succ < plus we are in the second case of the definition of <_{lpo} and therefore now have to show

       plus(x,y) <_{lpo} plus( x, succ(y) ).

In this case the leading function symbols are equal, so we are in the third case of the definition of <_{lpo} and it remains to be shown that

       (x,y) ≪_{lpo} (x,succ(y))

holds true. This last inequation follows from y <_{lpo} succ(y), which is true since y is a proper subterm of

succ(y).

3.3.3 The axioms section

The general form of an axiom section is this:

       begin( axioms ).

Named–Axiom_{1}.

⋮

Named–Axiom_{n}.

       end( axioms ).

The syntax of Named–Axiom is given as Name: Axiom Here Name is a unique name referring to this axiom, while Axiom is a \underline{closed} formula. Assigning a name to an axiom is a matter of convenience: Later on, it frees us from repeating long formulae over and over again. Instead, we can refer to them easily via their names.

10These equations should be ordered this way because they define addition on natural numbers. Since the left hand sides contain the terms which are to be defined these equations clearly should be ordered from left to right.

An alternative syntax for specifying axioms is given by the syntax

axiom( Named–Axiom ). This is convenient when specifying a single axiom.

In addition to the possibility of entering axioms directly via an axioms section, we have provided some convenient shorthands for dealing with certain types of axioms occurring frequently. These shorthands are described next. Although these shorthands belong logically to the axioms section, the may not be entered between the

       begin( axioms ) · · · end( axioms )

but have to be entered separately, either before or after the begin( axioms ) ⋯ end( axioms ) . We describe these shorthands next.

An ac declaration specifies a binary function f to be associative and commutative. f can only be specified as associative and commutative if there is a sort s such that the declaration of f takes the form:

       f:[s, s]  -> s.

The general form of an ac declaration, then, is the following:

       associative commutative( f ) .

Logically, this is equivalent to adding the axioms below stating the associativity and commutativity of f to the list of axioms:

       forall( [ x:s, y:s, z:s ], f(f(x,y),z) = f(x,f(y,z)) ).  (Associativity)
       forall( [ x:s, y:s ], f(x,y) = f(y,x) ).  (Commutativity)

Operationally, this is quite a different story. This is due to the fact that rewriting with these two equations involves a sorting procedure which can be implemented much more efficiently than ordinary rewriting. Therefore it is advisable to use ac declarations rather than the axioms of associativity and commutativity when a function is known to be associative and commutative.

aci declarations are similar to ac declarations. The only difference is that an operator declared to be aci is not only associative and commutative but also idempotent. So if f is declared via

       associative commutative idempotent( f ) .

as an aci operator, then this is logically equivalent to the following three axioms:

       forall( [ x:s, y:s, z:s ], f(f(x,y),z) = f(x,f(y,z)) ).  (Associativity)
       forall( [ x:s, y:s ], f(x,y) = f(y,x) ).  (Commutativity)
       forall( [ x:s ], f(x,x) = x ).  (Idempotence)

Concerning efficiency, the remark given above for ac declarations applies here as well.

If we want to make use of the built–in features dealing with inequalities (i.e., the relations <, >, =< and >=), we have to declare the sorts which are equipped with an ordering relation as linearly ordered. To declare the sort s as linearly ordered the command

       linear ordered( s ).

is used. Logically, this command is equivalent to the following axioms section:

       begin(axioms).
            forall( [ x:s, y:s ], x >= y  <-->  y =< x ).                 % Definition of ">="
            forall( [ x:s, y:s ], x < y  <-->  x =< y & ^x = y).         % Definition of "<"
            forall( [ x:s, y:s ], x > y  <-->  x >= y & ^x = y).         % Definition of ">"
            forall( x:s, x =< x ).                                       % Reflexivity
            forall( [ x:s, y:s ], x =< y & y =< x -> x = y ).             % Antisymmetry
            forall( [ x:s, y:s, z:s ], x =< y & y =< z -> x =< z ).       % Transitivity

            forall( [ x:s, y:s ], x =< y v y =< x ).                      % Linearity
       end(axioms).

Operationally, issuing a linear ordered command is, however, different from entering the axioms described above. This is due to the fact that the axioms are hard–wired into Seduct, which is much more efficient then adding them to the axiom part of Seduct’s database. Internally, an inequation “S =< T” is transformed into the equation “min srt( S, T ) = S” where srt is the sort of S and T. To this end after each linear ordered command Seduct internally declares the operator min srt via

min srt: [ srt, srt ] -> srt. The user is permitted to use this operator. The reflexivity, antisymmetry and transitivity of the ≤–relation are reflected by, respectively, the idempotence, symmetry, and associativity of the function “min srt”.

Furthermore, the axioms section may contain monotone declaration. The syntactical form of a monotone declaration for a function symbol f is given as

       monotone( f ) .

Logically, for all i ∈ {1, ⋯, n} this adds an axiom of the form

       u =< v  -> f(x_{1},· · ·,x_{i−1},u,x_{i+1},· · ·,x_{n}) =< f(x_{1},· · ·,x_{i−1},v,x_{i+1},· · ·,x_{n}).

(Of course, this formula has to be preceded by an appropriate universal quantifier. We have neglected this quantifier for reasons of space.) Operationally, instead of the axioms above we add rules of the following form to our rewrite calculus:

       min srt( f(x_{1},· · ·,x_{i−1},u,x_{i+1},· · ·,x_{n}), f(x_{1},· · ·,x_{i−1},v,x_{i+1},· · ·,x_{n}) ) =

       f(x_{1},· · ·,x_{i−1}, min srt(u,v), x_{i+1},· · ·,x_{n}).

These rules are added for all i ∈ {1, ⋯, n}.

Finally, an axioms section might contain so called generated declarations which give rise to induction rules. There are two types of generated declarations. The first takes the form:

       generated( s, [ f_{1}, · · ·, f_{k} ] ).

It asserts that the sort s is generated by the functions f_{1}, ⋯, f_{k}. This fact enables us later on to use induction rules which will be described further below. The functions f_{1}, ⋯, f_{k} will be referred to as constructors of the sort s. The second form of a generated declaration is

       freely generated( s, [ f_{1}, · · ·, f_{k} ] ).

In addition to enabling us to use induction rules, this declaration asserts the so called freeness axioms. These axioms can be dived into two groups, the injectivity axioms and the disjointness axioms. For each i ∈ {1, ⋯, k} there is one injectivity axiom of the form

       forall( [ x_{1}:s_{1},· · ·,x_{n}:s_{n}, y_{1}:s_{1},· · ·,y_{n}:s_{n} ],

               f_{i}(x_{1},· · ·,x_{n}) = f_{i}(y_{1},· · ·,y_{n}) -> x_{1} = y_{1} & · · · & x_{n} = y_{n} ).

For each pair of integers i, j ∈ {1, ⋯, k} with i ≠ j there is one disjointness axiom of the form

       forall( [ x_{1}:s_{1},· · ·,x_{n}:s_{n}, y_{1}:s_{1},· · ·,y_{n}:s_{m} ], ^f_{i}(x_{1},· · ·,x_{n}) = f_{j}(y_{1},· · ·,y_{m}) ).

Since injectivity and disjointness of functions are concepts which are not only useful when dealing with freely generated datatypes, there are separate commands for their declaration. Declaring a function f as injective is achieved via the injective declaration

       injective( f ).

and to declare the functions f and g to be disjoint we can use

       disjoint( f, g ).

Operationally these axioms are hardwired into the rewriting calculus.

3.3.4 The definitions section

The general form of a definitions section is the following:

       begin(definitions).

Named–Definition_{1}.

⋮

Named–Definition_{n}.

       end(definitions).

An alternative syntax for specifying a definition is given by the syntax

definition( Named–Definition ). A named definition defines either a function or a predicate. The general syntax for a named definition is as follows:

Name: Definition Here Name is a unique name which can be used to refer to this definition. Definition is a definition. Definitions come in two forms and for each form there are two variants. The different forms are due to the fact that we can define either a function or a predicate. The different variants are caused by the fact that we can use conditional definitions as well as unconditional ones.

If a function f of n arguments is to be defined unconditionally, the syntax of Definition is^{11}

       forall( [x_{1}:s_{1}, · · ·, x_{m}:s_{m}], f(t_{1}, · · ·, t_{n}) = t )

where t is the term defining the function f for the arguments t_{1}, ⋯, t_{n} and x_{1}, ⋯, x_{m} is the list of all variables appearing in the terms t_{1}, ⋯, t_{n}. Furthermore, the definition is only legal if every variable appearing on the right hand side of the equation appears also on the left hand side of the equation, i.e., we must have

FV (t) ⊆ FV (t_{1}) ∪ ⋯ ∪ FV (t_{n}).

If the definition is conditional, the syntax is

       forall( [x_{1}:s_{1}, · · ·, x_{m}:s_{m}], Condition -> f(t_{1}, · · ·, t_{n}) = t )

where Condition is a conjunction of literals. (Remember that literals are prime formulae or negated prime formulae.) A conditional definition of a function must satisfy the following condition:

FV (t) ∪ FV (Condition) ⊆ FV (t_{1}) ∪ ⋯ ∪ FV (t_{n}),

i.e., every variable appearing in the condition or in the right hand side has to appear in the term to be defined.

To define a predicate p of n arguments the syntax of an unconditional Definition is as follows:

       forall( [x_{1}:s_{1}, · · ·, x_{m}:s_{m}], p(t_{1}, · · ·, t_{n}) <--> F )

where F is the formula determining the truth value of p for the arguments t_{1}, ⋯, t_{n} and x_{1}, ⋯, x_{m} is the list of all variables appearing in the terms t_{1}, ⋯, t_{n}. Furthermore, the definition is only legal if every variable appearing free on the right hand side of the definition appears also on the left hand side of the definition, i.e.,

F V (F) ⊆ F V (t_{1}) ∪ ⋯ ∪ F V (t_{n}).

The conditional variant for predicate definitions is given as

forall( [x_{1}:s_{1}, ⋯, x_{m}:s_{m}], Condition -> p(t_{1}, ⋯, t_{n}) <--> F ) , where Condition is a conjunction of prime formulae. In this case the variable condition reads

FV (F) ∪ FV (Condition) ⊆ FV (t_{1}) ∪ ⋯ ∪ FV (t_{n}).

Very often when defining a predicate, the formula on the right hand side of a definition is either true or false. For this case there are some shortcuts available. A definition of the form

       forall( [x_{1}:s_{1}, · · ·, x_{m}:s_{m}], p(t_{1}, · · ·, t_{n}) <--> true )

11Of course, if FV (t) = ∅, i.e., if the term t is closed, the definition above becomes

f(t_{1}, ⋯, t_{n}) = t In the future, we will tacitly assume that we can drop unnecessary quantifiers.

may be written as

forall( [x_{1}:s_{1}, ⋯, x_{m}:s_{m}], p(t_{1}, ⋯, t_{n}) ) , while a definition of the form

       forall( [x_{1}:s_{1}, · · ·, x_{m}:s_{m}], p(t_{1}, · · ·, t_{n}) <--> false )

is more conveniently given as

       forall( [x_{1}:s_{1}, · · ·, x_{m}:s_{m}], ^p(t_{1}, · · ·, t_{n}) ) .

Of course, the same shortcuts are available for conditional definitions.

Logically, a definition is equivalent to an axiom. It can be used at any place where an axiom can be used. Operationally, things are different because definitions can be expanded. By this means the usage of a definition can be controlled much better than the usage of an axiom. We will explain this point in more detail when discussing the expand and the expand all command.

3.3.5 The goals section The general form of a goals section is this:

       begin(goals).

Named–Goal_{1}. ⋮ Named–Goal_{n}.

       end(goals).

Alternatively, if we want to define just one goal, the syntax

goal( Named–Goal ) . is sufficient. The syntax of a goal is given by

Name: Goal Here Name is a unique name referring to this goal, while Goal is a \underline{closed} formula. Goals are formulae which we want to prove.

3.3.6 The theories section The general form of a theories section is this:

       begin(theories).

Theory–Definition_{1}.

⋮ Theory–Definition_{n}.

       end(theories).

An alternative syntax for specifying just a single theory is given as

theory( Theory–Definition ). A theory definition is just a convenience for collecting axioms and theorems. The prototype of a theory definition is the following:

Name = Theory Observe that Name and Theory are separated by an equality sign “=” and not by a colon “:” as used with axioms and definitions. In this definition Name is a name for the new theory to be declared and Theory can have either of the following two forms:

1. Theory might be a list of names: [ Name_{1}, ⋯, Name_{n} ] Each of the names above must be either the name of an axiom, a definition, a theorem, or the name of a goal. If a theory contains a name of a goal, it can only be used for a proof only \underline{after} this goal has been proved and thereby turned into a theorem.

2. Theory might be the sum of already defined theories. In this case the syntax is: Theory_{1} + Theory_{2} where Theory_{1} and Theory_{2} are themselves theories. With this definition Theory contains all the axioms, definitions and theorems contained in either Theory_{1} or Theory_{2}.^{12}

3.3.7 The proofs section

This is now the final, and by far most interesting, section of a command file. It consists of a sequence of commands, each on a different line and followed bu a “.”. The complete set of commands available will be described in section 7. For now, we will sketch only some of the most important commands.

The first command is the prove command. Its syntax is:

prove( Name, Theory ). Here Name has to be the name of a goal and Theory is a collection of axioms which will be used in the proof of the formula referred to by Name. Executing this command switches Seduct from into the prove mode and changes the prompt from the normal

       SEDUCT>

to

       SEDUCT(Name):

Furthermore, the formula referred to by Name is pushed on the top of a newly created goal stack.

The other commands we will describe can only be executed in prove mode. The first is the go command. Its syntax is very simple:

       go.

It causes Seduct to try to do the proof of the current goal, i.e., the goal on top of the goal stack, by pure first order methods. (These methods will be described in Section 5 and Section 6.) If the proof succeeds, the goal which has been proved is removed from the goal stack. If it was the last formula on the goal stack, then the corresponding goal is converted into a theorem which can then be used in future proofs. If the go command were the only command in prove mode, then every goal stack produced would consist of just one goal. The commands available for induction change this situation.

There are two commands concerned with induction. The first is the induction command. Its syntax is

       induction( x ).

This command can only be used if there exists a generated or freely generated declaration for the sort s of the variable x. Furthermore, the current goal has to be a universally quantified formula. The effect of the induction command is to prove the current goal via structural induction on x. How this works exactly will be described in a section 7. For now it is sufficient to know that it will create a new subgoal for every constructor appearing in the generated or freely generated declaration for the sort s. These subgoals then have to be proved recursively. If the sort nat representing natural numbers is equipped with the generated clause

       generated( nat, [ zero, succ ] ).

this will just amount to an ordinary inductive proof step. If the formula to be proved is

       forall( x:  nat, F ),

then the command induction(x) replaces the current goal with the following two goals:

   1. forall( x:  nat, F[x <- zero] ),

12Internally, theories are represented as lists. If we use an expression of the form

Theory = Theory_{1} + Theory_{2} then the internal representation of Theory is computed by appending the lists representing Theory_{1} and Theory_{2}. Therefore, if an axioms occurs both in Theory_{1} and Theory_{2}, then it will occur twice in the list representing Theory.

2. forall( x:  nat, F[x <- cn] -> F[x <- succ(cn)] ),

(Here cn is a new constant generated by Seduct and F[x <- T] denotes the formula obtained from F by replacing every occurrence of x in F with T.) The goals pushed on the stack can then be proved with further commands.

We illustrate the use of the commands described so far via an example. Assume that declarations, axioms, goals and theories have been defined via the following commands:

begin( declare ).
      zero: nat.
      succ: [ nat ]       ->  nat.
      plus: [ nat, nat ]  ->  nat.
end( declare ).
begin( axioms ).
     plus_zero: forall( x: nat, plus( x, zero ) = x ).
     plus_succ: forall( [ x: nat, y: nat ], plus( x, succ(y) ) = succ( plus(x,y) ) ).
end( axioms ).
freely_generated( nat, [ zero, succ ] ).
begin( operators ).
     zero: 0.
     succ: 1.
     plus: 2.
end( operators ).
begin( goals ).
      associativity: forall( [ x:nat, y:nat, z:nat ],
                             plus( plus(x,y), z ) = plus( x, plus(y,z) )
                           ).
      commutativity: forall( [x:nat, y:nat],
                             plus(x,y) = plus(y,x)
                           ).
end( goals ).
begin( theories ).
      pl = [ plus_zero, plus_succ ].
      ac = [ associativity, commutativity ].
end( theories ).

To try the following example we can either enter these definitions as given above, or we can alternatively enter them into a file. However, in this case the file should contain an additional

    quit.

as the last command in order to close the file on execution. Let us assume there is such a file. Let us further assume^{13} that the file containing these declarations is

    /home/x2000/karl/SEDUCT/Doc/peano.sed

If this assumption is true, then issuing the command

    execute( '/home/x2000/karl/SEDUCT/Doc/peano.sed' ).

13Well, we do not have to assume it. The file really exists at the location below. And after all, if you cannot mount from x2000 that is your problem.

will have the same effect as entering all the declarations above.^{14} If we want to assure us that we have loaded the right axioms, we can view them via the show( axioms ) command. After issuing this command we see the following:

    SEDUCT> show( axioms ).
    plus_zero : forall(x : nat,plus(x,zero) = x)
    plus_succ : forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
    SEDUCT>

There are some variants of the show commands for viewing declarations, definitions, goals and theories. These will be described in Section 7.

In order to be able to watch what is going on we issue the command

       set( show( complete ) ).

which shows the goal on top of the goal stack every time it changes. We start with the proof of the associativity of addition by entering the command

       prove( associativity, pl ).

This will result in the following output:

    SEDUCT> prove( associativity, pl ).
        % Now proving: "associativity".
    Antecedent:
     (1)  forall(x : nat,plus(x,zero) = x)
     (2)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
    Succedent:
     (1)  forall([x : nat,y : nat,z : nat],plus(plus(x,y),z) = plus(x,plus(y,z)))
    SEDUCT(associativity):

To understand this output we have to note that Seduct works via a sequent calculus when proving formulae. A sequent is a pair of lists of formulae. The first component of this list is called antecedent. It can be seen as a list of axioms from which to prove any of the formulae in the second list wich is called succedent. Usually this second list will contain just a single formula. To proceed, we try to prove the current goal via induction on the variable z via the command

       induction( z ).

After entering this command we will see the following response:

    SEDUCT(associativity): induction( z ).
            % Now proving: "associativity_ind_1".
    Antecedent:
     (1)  forall(x : nat,plus(x,zero) = x)
     (2)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
    Succedent:
     (1)  forall([x : nat,y : nat],plus(plus(x,y),zero) = plus(x,plus(y,zero)))
    SEDUCT(associativity_ind_1):

14We have to include the file name in quotes since it contains uppercase variables and these would be taken as Prolog variables if we had entered the file name without quotes.

So we now are no in the base case of the induction and we have to prove

       plus( plus(x,y), zero ) = plus( x, plus(y,zero) )

which follows easily from the first formula in the antecedent of the current goal. Therefore we try the go command next, getting the response

    SEDUCT(associativity_ind_1): go.
                % Proof of "associativity_ind_1" finished.
            % Now proving: "associativity_ind_2".
    Antecedent:
     (1)  forall([x : nat,y : nat],plus(plus(x,y),c2) = plus(x,plus(y,c2)))
     (2)  forall(x : nat,plus(x,zero) = x)
     (3)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
    Succedent:
     (1)  forall([x : nat,y : nat],plus(plus(x,y),succ(c2)) = plus(x,plus(y,succ(c2))))
    SEDUCT(associativity_ind_2):

The message “% Proof of "associativity ind 1" finished.” tells us that we were successful with the base case. Below that message we are given the new subgoal to prove. Since we are now in the step case we have the induction hypothesis

       plus( plus(x,y), c2 ) = plus( x, plus(y,c2) )

at our disposal. Therefore the antecedent contains now three formulae. If we procceed via the “go” command, the proof succeeds and we get the response:

    SEDUCT(associativity_ind_2): go.
            % Proof of "associativity_ind_2" finished.
        % Proof of "associativity" finished.
    SEDUCT>

We are now ready to tackle the problem of commutativity. We start the proof by typing

    prove( commutativity, pl ).

We get the system response

    % Now proving: "commutativity".
    Antecedent:
     (1)  forall(x : nat,plus(x,zero) = x)
     (2)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
    Succedent:
     (1)  forall([x : nat,y : nat],plus(x,y) = plus(y,x))
    SEDUCT(commutativity):

We try to carry on via an induction on x. We get the following response:

    SEDUCT(commutativity): induction( x ).
        % Now proving: "commutativity_ind_1".

Antecedent:
 (1)  forall(x : nat,plus(x,zero) = x)
 (2)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
Succedent:
 (1)  forall([y : nat],plus(zero,y) = plus(y,zero))
SEDUCT(commutativity_ind_1):

Now we try a new command. It is the command “expand all”. The effect of this command is to use all available definitions together with the formulae in the antecedent to simplify the sequent currently being proved. In our case the system contains no definitions, but the equation

   plus( x, zero ) = x

in the antecedent can be used to simplify the term

   plus( y, zero )

in the succedent. So issuing this command leaves us with

SEDUCT(commutativity_ind_1): expand_all.
Antecedent:
 (1)  forall(x : nat,plus(x,zero) = x)
 (2)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
Succedent:
 (1)  forall([y : nat],plus(zero,y) = y)
SEDUCT(commutativity_ind_1):

If we try to carry on via a “go” command, we get the response

SEDUCT(commutativity_ind_1): go.
% Proof suspended.
SEDUCT(commutativity_ind_1):

What has happened? The answer is quite simple: The formula

forall(x : nat,plus(x,zero) = x)                              &
forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))   ->
forall([y : nat],plus(zero,y) = y)

is not a theorem of first order logic! Instead, we have to prove it via induction. So we carry on via the command sequent

induction( y ).
go.
go.

After the last of these “go” commands we get the message

SEDUCT(commutativity_ind_1_ind_2): go.
            % Proof of "commutativity_ind_1_ind_2" finished.
        % Proof of "commutativity_ind_1" finished.
    % Now proving: "commutativity_ind_2".
Antecedent:

 (1)  forall([y : nat],plus(c2,y) = plus(y,c2))
 (2)  forall(x : nat,plus(x,zero) = x)
 (3)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
Succedent:
 (1)  forall([y : nat],plus(succ(c2),y) = plus(y,succ(c2)))
SEDUCT(commutativity_ind_2):

This informs us that we have successfully completed the side induction in the base case and are now in the induction step of the main induction. Trying the “expand all” command again we get the message

SEDUCT(commutativity_ind_2): expand_all.
Antecedent:
 (1)  forall([y : nat],plus(c2,y) = plus(y,c2))
 (2)  forall(x : nat,plus(x,zero) = x)
 (3)  forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y)))
Succedent:
 (1)  forall([y : nat],plus(succ(c2),y) = succ(plus(y,c2)))
SEDUCT(commutativity_ind_2):

In analogy to the base case we try to solve this goal via a side induction on the variable y. This works fine, since after executing the command sequence

induction( y ).
go.
go.

we get the response

SEDUCT(commutativity_ind_2_ind_2): go.
            % Proof of "commutativity_ind_2_ind_2" finished.
        % Proof of "commutativity_ind_2" finished.
    % Proof of "commutativity" finished.
SEDUCT>

We can check that we really have achieved our goals by entering the command “show( theorems )”. This will give us the response:

SEDUCT> show( theorems ).
associativity : forall([x : nat,y : nat,z : nat],plus(plus(x,y),z) = plus(x,plus(y,z)))
commutativity : forall([x : nat,y : nat],plus(x,y) = plus(y,x))
SEDUCT>

So our original goals have indeed been converted into theorems. Finally, we leave the system by typing

exit.

During our session Seduct has written a file logging our commands. This file does not only log our commands but gives also some comments on the proof. As a matter of fact, we think that files of this style provide efficient means for communicating proofs. We have listed this file below.

% '/home/x2000/karl/SEDUCT/Doc/peano.sed'.
begin(declare).
    zero : nat.
    succ : [nat] -> nat.
    plus : [nat,nat] -> nat.
end(declare).
begin(axioms).
    plus_zero : forall(x : nat,plus(x,zero) = x).
    plus_succ : forall([x : nat,y : nat],plus(x,succ(y)) = succ(plus(x,y))).
end(axioms).
freely_generated(nat,[zero,succ]).
begin(operators).
    zero : 0.
    succ : 1.
    plus : 2.
end(operators).
begin(goals).
    associativity : forall([x : nat,y : nat,z : nat],plus(plus(x,y),z) = plus(x,plus(y,z))).
    commutativity : forall([x : nat,y : nat],plus(x,y) = plus(y,x)).
end(goals).
begin(theories).
    pl = [plus_zero,plus_succ].
    ac = [associativity,commutativity].
end(theories).
set(show(complete)).
prove(associativity,pl).
% Now proving: "associativity".
    induction(z).
    % Now proving: "associativity_ind_1".
        go.
        % Proof of "associativity_ind_1" finished.
    % Now proving: "associativity_ind_2".
        go.
        % Proof of "associativity_ind_2" finished.
    % Proof of "associativity" finished.
prove(commutativity,pl).
% Now proving: "commutativity".
    induction(x).
    % Now proving: "commutativity_ind_1".
        expand_all.
        go.
% Proof suspended.
        induction(y).
        % Now proving: "commutativity_ind_1_ind_1".
            go.
            % Proof of "commutativity_ind_1_ind_1" finished.
        % Now proving: "commutativity_ind_1_ind_2".

go.
% Proof of "commutativity_ind_1_ind_2" finished.
% Proof of "commutativity_ind_1" finished.
% Now proving: "commutativity_ind_2".
expand_all.
induction(y).
% Now proving: "commutativity_ind_2_ind_1".
go.
% Proof of "commutativity_ind_2_ind_1" finished.
% Now proving: "commutativity_ind_2_ind_2".
go.
% Proof of "commutativity_ind_2_ind_2" finished.
% Proof of "commutativity_ind_2" finished.
% Proof of "commutativity" finished.
exit.

4 Verification of Algorithms with SEDUCT

In this section we want to describe how Seduct can be used to verify the correctness of algorithms. Furthermore, this section gives some hints showing how to work efficiently with Seduct. We will start with the verification of a small sorting algorithm, namely the insertion sort algorithm.

4.1 Verification of the Insertion Sort Algorithm

The insertion sort algorithm is one of the most straightforward sorting algorithms. Its main idea is to perform the sorting procedure inductively:

1. If the list to sort is empty, we return the empty list:

             return( [] ).

2. Otherwise the list has the form

             [ X | Xs ]

with head X and tail Xs. In this case we proceed recursively:

(a) We sort the tail Xs to produce

                     Sorted-Xs := isort( Xs ).

(b) After that we insert the head X into the sorted tail at the right place and return the resulting

list

                     return( insert( X, Sorted-Xs ) ).

To formulate this procedure in Seduct we need the notion of lists together with functions for inserting an element into a list and a function to sort lists. The following declare section will introduce the notions needed.

    begin( declare ).
        []:                             list.
        '.':     [ element, list ]  ->  list.
        insert:  [ element, list ]  ->  list.
        isort:   [ list ]           ->  list.
    end( declare ).

We should comment on the declaration of the dot “.”. The dot is the Prolog constructor for lists. The Prolog parser used by Seduct internally converts an expression of the form

[ Head | Tail ] into

'.'( Head, Tail ). Thus, to be able to use the former notation, we have to declare a function “.” appropriately.

Since list are freely generated from the empty list “[]” and the cons operator “.”, we issue the command

       freely generated( list, [ [], '.'  ]  ).

Again, we have written the dot “.” in quotes. This is necessary since the dot is declared as an infix operator in Seduct.

In order to be able to sort lists we have to assume that =< is a linear order on the sort element. Therefore we issue the command

    linear_ordered( element ).

We can proceed with the definition of the insertion sort algorithm. This is achieved via the following definitions section. To be able to write it succinctly we declare the function isort as a prefix operator. This can be done via the “op” command. Its syntax is the same as in Prolog. It is fully explained in Section 7. In our case, the command

    op( 10, fx, isort ).

is what is needed. Next we can define the functions insert and isort:

   begin( definitions ).
       % Axioms defining insert:
       insert_1: forall( x: element, insert( x, [] ) = [ x ] ).
       insert_2: forall( [x: element, y: element, l:list],
                 insert( x, [ y | l ] ) = if( x=< y, [ x, y | l ], [ y | insert(x,l) ] ) ).
       % Axioms defining isort
       isort_1: isort [] = [].
       isort_2: forall( [x:element, l:list], isort [ x | l ] = insert(x, isort l) ).
   end( definitions ).

Our aim is to show that the result of sorting a list is an ordered list. To be able to formulate this we first have to declare a predicate ordered and we have to define this predicate. Basically, a list is ordered if it is either the empty list or it is a list of the form “[ Head | Tail ]” where Tail is ordered and Head is less or equal than the first element of Tail. To be able to write this succinctly, we will introduce the notion “=<<”. The statement

       x =<< l

holds true between an element x and a list l if and only if the element x is less or equal than the head of the list l. To increase readability we will declare the predicate ordered as a prefix operator while =<< will be declared as an infix operator. These declarations are done via the following commands.

    arity( ordered: [ list ] -> bool ).
    arity( =<< : [ element, list ] -> bool ).
    op( 10, xfx, =<< ).
    op( 10, fx, ordered ).

Observe that we have to separate the symbol “=<<” and the colon “:” via a blank since otherwise Seduct would interpret “=<<:” as a single symbol. You might be wondering why we did not include the symbol “=<<” in quotes in the arity declaration:

       arity( =<< :  [ element, list ] -> bool ).

There was no necessity for using quotes then, since at the time of the arity declaration the symbol “=<<” had not yet been declared as an infix operator.

The definition of “=<<” and “ordered” is now achieved via the following commands:

    begin( definitions ).
        % Axioms for =<<
        '=<<_1': forall( x: element, x =<< [] ).
        '=<<_2': forall( [ x: element, y: element, l: list ],
                         x =<< [ y | l ]  <-->  x =< y ).
        % Axioms for ordered:
        ord1: ordered [].
        ord2: forall( [ x: element, l: list ],
                      ordered [ x | l ]  <-->  x =<< l & ordered l ).
    end( definitions ).

In the string “'=<< 1'” the quotes are necessary since the string “=<< 1” consists of characters from two different classes: “=”, “<” and “>” are characters from the lexical class denoted as special characters, while “ ” and “1” are characters from the class denoted as letters, digits, and underscore. Therefore, without the quotes the Prolog parser would have recognized two tokens, namely “=<<” and “ 1”.

Next we can specify the goals. First of all we want to prove something like

       forall( l:  list, ordered( isort l ) ).

We will, however, not be able to prove this directly but will need some lemmata describing our domain theory. We have made the experience that these lemmata often take the form of distribution laws showing how certain more complex notions distribute over simpler ones. In our case, the notion of a list being ordered is more complex than the notion of inserting an element into a list. We therefore have to formulate a distribution law telling us how ordered distributes over insert. The distribution law required takes the form:

       ordered insert( x, l )  <-->  ordered l,

i.e., the result of inserting x into the list l is ordered if and only if l is ordered. Since the predicate ordered is defined with the help of the predicate =<<, it will be necessary to derive a second distribution law telling us how to distribute =<< over insert. This law reads

       x =< y  ->  ( x =<< insert( y, l )  <-->  x =<< l ),

i.e., x is less then the head of the list resulting from inserting x into l iff x is less than the head of l provided that x =< y holds. The condition x =< y is needed to ensure that the reverse direction of the equivalence holds. We need to formulate our distribution laws as equivalences since otherwise it would not be possible to use them for rewriting, i.e., if we had only formulated the last distribution law as

       ( x =<< insert( y, l )  ->  x =<< l ),

then we would not be able to use it to simplify expressions of the form

       s =<< insert( t, l ).

We state all the lemmata and our original goal in the following goal section:

    begin( goals ).
        lemma_1: forall( [ x:element, y:element, l:list ],
                          x =< y  ->  ( x =<< insert(y,l)  <-->  x =<< l )
                       ).
        lemma_2: forall( [x:element, l:list],
                         ordered insert(x,l)  <-->  ordered l
                       ).
        theorem: forall( [l: list],
                         ordered( isort l )
                       ).
    end( goals ).

Now we are ready to start the proof. We will have to prove all of our goals via induction. However, we will not use structural induction, but use a concept known as computational induction or lazy induction. This concept has been introduced by Boyer and Moore [2]. If a function f is defined recursively via a set of k conditional equations of the form

C_{i} → f(A_{i0}) = t_{i}( f(A_{i1}), ⋯, f(A_{im_{i}}) ), with i running over the set {1, ⋯, k}, then in order to prove a formula

       forall( x:S, F( f(x) ) )

it is sufficient to prove for all i ∈ {1, ⋯, k} the following:

C_{i} & F( f(A_{i1}) ) & ⋯ & F( f(A_{im_{i}}) ) -> F( t_{i}( f(A_{i1}), ⋯, f(A_{im_{i}}) ) ). However, this induction rule is only applicable if the definition of f does not contain the if operator. If a definition is of the form

C -> f(s_{1}, ⋯, s_{n}) = if( B, t_{1}, t_{2} )

then this definition is first transformed into two definitions of the form

B & C -> f(s_{1}, ⋯, s_{n}) = t_{1} and

^B & C -> f(s_{1}, ⋯, s_{n}) = t_{2}.

In our case, the definition of the function insert is converted into the equivalent definition

    insert( x, [] ) = [ x ] ).
    x =< y  ->  insert( x, [ y | l ] ) = [ x, y | l ].
  ^x =< y  ->  insert( x, [ y | l ] ) = [ y | insert(x,l) ].

Therefore, if we want to prove a goal of the form

       forall( [ x:  element, l:  list ], F( insert( x, l ) ) )

via lazy induction, then we will have to prove three subgoals, namely

   1. forall( [ x:element, l:list ],
             F( [ x ] ) ),
   2. forall( [ x:element, y:element, l:list ],
             x =< y -> F( [ x, y | l ] ) ),
   3. forall( [ x:element, y:element, l:list ],
             ^x =< y & F( insert( [y|l] ) ) -> F( [ y | insert(x,l) ] ) ) .

With this explanation in mind we can proceed to prove lemma 1 via lazy induction. After typing

       set( show( complete ) ).
       prove( lemma 1, [] ).
       lazy induction( insert ).

the situation is as follows:

SEDUCT(lemma_1): lazy_induction( insert ).
    % Now proving: "lemma_1_lazy_1".
Succedent:
 (1)  c7 =< c3 -> (c7 =<< [c3] <--> c7 =<< [])
SEDUCT(lemma_1_lazy_1):

Entering the command

       expand all.

leaves us with

Succedent:
 (1)  c7 =< c3 -> c7 =< c3

which is obviously trivial. After entering “go.” we therefore proceed to the next subgoal:

        % Proof of "lemma_1_lazy_1" finished.
    % Now proving: "lemma_1_lazy_2".
Antecedent:
 (1)  c4 =< c5

Succedent:
 (1)  c10 =< c4 -> (c10 =<< [c4,c5|c6] <--> c10 =<< [c5|c6])
SEDUCT(lemma_1_lazy_2):

This subgoal is again dealt with by the command sequence

       expand all.
       go.

After that we get the following message:

        % Proof of "lemma_1_lazy_2" finished.
    % Now proving: "lemma_1_lazy_3".
Antecedent:
 (1)  ^c4 =< c5
 (2)  c13 =< c4 -> (c13 =<< insert(c4,c6) <--> c13 =<< c6)
Succedent:
 (1)  c13 =< c4 -> (c13 =<< [c5|insert(c4,c6)] <--> c13 =<< [c5|c6])
SEDUCT(lemma_1_lazy_3):

This is now the induction step. The second formula in the antecedent contains our induction hypotheses. After typing

       expand all.

the formula

       c13 =< c4 -> (c13 =<< [c5|insert(c4,c6)] <--> c13 =<< [c5|c6])

in the succedent is first reduced to

       c13 =< c4 -> (c13 =< c5 & c13 =<< insert(c4,c6) <--> c13 =< c5 & c13 =<< c6 ).

However, this formula is not displayed since now the induction hypotheses can be used to expand the term

       c13 =<< insert(c4,c6)

into

       c13 =<< c6

This expansion leaves us with

       c13 =< c4 -> (c13 =< c5 & c13 =<< c6 <--> c13 =< c5 & c13 =<< c6) .

Since now the formula c13 =< c5 & c13 =<< c6 appears on both sides of the equivalence <-->, this last formula is trivially seen to be true. Therefore the net effect of the “expand all” command this time is just

SEDUCT(lemma_1_lazy_3): expand_all.
Antecedent:
 (1)  ^c4 =< c5
 (2)  c13 =< c4 -> (c13 =<< insert(c4,c6) <--> c13 =<< c6)
Succedent:
 (1)  true
SEDUCT(lemma_1_lazy_3): go.
        % Proof of "lemma_1_lazy_3" finished.
    % Proof of "lemma_1" finished.
SEDUCT>

So we have finished the proof of lemma 1. Let us see whether we can learn something from it. The proof went via induction and required no further interaction besides the “expand all” and “go” commands. Maybe we can prove lemma 2 the same way. And wouldn’t it be nice if we could somehow automatize this procedure? Well, that is possible since we can use a parameterized macro. A parameterized macro serving our purposes can be defined as follows:

  macro( auto_induction, goal, fn, theory ).
      prove( goal, theory ).
          lazy_induction( fn ).
              expand_all.
              go.
              expand_all.
              go.
              expand_all.
              go.
  end( auto_induction ).

The idea of this macro is easy to understand. First the formula referred to by “goal” is put on the top of the goal stack. This formula is proved via lazy induction according to the definition of the function “fn”. Each case is then solved by first expanding all definitions and then executing the “go” command. Let us try our macro on lemma 2. We first use the command

       unset( show( complete ) ).

to switch off the display facility. This is advisable in order not to get cluttered with uninteresting information. After that issuing the command

       auto induction( lemma 2, insert, [ lemma 1 ] ).

causes our macro to do the proof of lemma 2 via lazy induction using lemma 1. The output generated by Seduct is:

    SEDUCT> auto_induction( lemma_2, insert, [ lemma_1 ] ).
    % Now proving: "lemma_2".
        % Now proving: "lemma_2_lazy_1".
            % Proof of "lemma_2_lazy_1" finished.
        % Now proving: "lemma_2_lazy_2".
            % Proof of "lemma_2_lazy_2" finished.
        % Now proving: "lemma_2_lazy_3".
            % Proof of "lemma_2_lazy_3" finished.
        % Proof of "lemma_2" finished.

This shows that our guess was right and lemma 2 can indeed be proven the same way as lemma 1. Since lemma 2 has got the form of a definition, it might be useful to use it when expanding terms via the “expand all” command. To achieve this, we issue the command

       use as definition( lemma 2 ).

This command converts lemma 2 from a theorem into a definition.

Now all that remains to be done is to prove the goal named “theorem”. This time the proof is carried out via an ordinary structural induction. Since the sort list is generated by the constructors “[]” and “.”, in order to prove a formula of the form

       forall( [ l:list ], F(l) )

via structural induction we have to prove two subgoals:

   1. F([]) ).
   2. forall( [ x:element, l:list ], F(l) -> F([x|l]) ).

We start the proof of theorem after switching the display facility via “set( show( complete ) )” on again by issuing the command

       prove( theorem, [] ).

This results in the output

% Now proving: "theorem".
Succedent:
 (1)  forall([l : list],ordered isort l)

We proceed via structural induction on l:

       induction( l ).

In the base case, we have to prove

Succedent:
 (1)  ordered isort []

This goal can be solved via the commands

       expand all.
       go.

After that we are left with:

    % Now proving: "theorem_ind_2".
Antecedent:
 (1)  ordered isort c1
Succedent:
 (1)  ordered isort [c0|c1]

After “expand all” the situation changes into

Antecedent:
 (1)  ordered isort c1
Succedent:
 (1)  true

and we can finish the proof with the “go” command. Now we are ready to mix ourselves a drink because we have just verified our first algorithm.^{15}

4.2 Verification of the Correctness of the Quicksort Algorithm

In this section we will use Seduct to prove that a list that has been sorted by the quicksort algorithm really is ordered. In the first part, it is shown how such a proof can be developed in Seduct, and in a second part, this proof is rewritten using macros to make it is easier to read.

The quicksort algorithm sorts a list by splitting it up into two lists which are sorted separately and then concatenated. More concretely:

15As a matter of fact, we have only verified one half of the intended properties of the insertion sort algorithm. We have shown that the result of the insertion sort algorithm is ordered. Of course, implementing a function satisfying only this requirement is trivial:

just take a function always returning the empty list! What remains to be shown is the fact that the list isort(l) contains exactly the same elements as the list l.

1. If the list to be sorted is empty, the sorted list is, of course, empty, too.

      qs([]) = []

2. If the list is not empty, an arbitrary element from the list is chosen as pivot element^{16}. The remaining elements of the list are separated into two lists: one containing those elements that are smaller than the pivot element, and one containing those that are greater than or equal to the pivot element. These two lists are sorted separately, and the resulting lists are concatenated with each other and the pivot element:

      qs(x@l) = qs(small part(x,l)) * x @ qs(big part(x,l))

where @ adds an element to the head of a list, * concatenates two lists, small part selects those elements of a list that are smaller than the pivot element, and big part selects those elements that are greater than or equal to the pivot element.

4.2.1 The Specification

To specify the quicksort algorithm in Seduct, we need the notion of a list with the operations used above. The necessary operators are declared by the following declare section:^{17}

begin(declare).
   ([]): list.
   (@): [ element, list] -> list.
   (*): [ list, list] -> list.
   small part: [ element, list] -> list.
   big part: [ element, list] -> list.
end(declare).

To avoid problems parsing predefined operators, operators consisting of special symbols (cf. appendix A) are enclosed in parentheses^{18}. The function symbols that are to be used as infix operators are declared as such and given appropriate priorities with the commands:

op( 10, xfy, @).
op( 15, xfy, *).

and the facts that element is ordered and that list is freely generated by [] and @ are specified by the following commands:

linear ordered(element).
freely generated( list, [ ([]), (@)]).

We are now ready to specify the properties of our list operations. This is done in the following definitions section:

begin(definitions).
   append1: forall( l: list, [] * l = l).
   append2: forall( [ x: element, l: list, k: list], x@l * k = x @ (l * k)).
   s1: forall( x: element, small part(x,[]) = []).
   s2: forall( [ x: element, y: element, l: list],
      small part(x,y@l) = if( y < x, y @ small part(x,l), small part(x,l))).
   b1: forall( x: element, big part(x,[]) = []).
   b2: forall( [ x: element, y: element, l: list],
      big part(x,y@l) = if( y >= x, y @ big part(x,l), big part(x,l))).

16To simplify the specification, we always choose the first element.

17The operators used in this section are different from those used in the previous section on the insertion sort algorithm.

18Actually, neither [], @ nor * is predefined and, thus, neither had to be parenthesized.

      end(definitions).

Having defined the necessary operations on lists, we can continue with the definition of the quicksort algorithm:

      arity( qs: [list] -> list).
      op( 10, fy, qs).
      begin(definitions).
         qs1: qs [] = [].
         qs2: forall( [ x: element, l: list],
           qs x@l = qs small part(x,l) * x @ qs big part(x,l)).
      end(definitions).

In order to save a level of parentheses in larger formulae, we have specified qs as a prefix operator with a pretty high priority, i.e. binding as strong as @.

We have now completed the specification of the quicksort algorithm, and continue with the first requirement for the correctness of the algorithm: that the elements of the sorted list are indeed ordered. For this purpose we introduce a new operation on lists =<< which compares an element with all elements in a list.

      begin(declare).
         (=<<): [ element, list] -> bool.
         ordered: [list] -> bool.
      end(declare).
      op( 25, xfx, =<<).
      begin(definitions).
         '=<< 1': forall( x: element, x =<< []).
         '=<< 2': forall( [ x: element, y: element, l: list],
           x =<< y@l <--> x =< y & x =<< l).
         ord1: ordered([]).
         ord2: forall( [ x: element, l: list], ordered(x@l) <--> x =<< l & ordered(l)).
      end(definitions).

The specification is now finished, and we can formulate the property we want to prove: that any list that has been sorted by qs is ordered.

      goal( th1: forall( [ l: list], ordered(qs l))).

4.2.2 The Proof Development

We now start developing the proof after having told Seduct to display the sequent to be proven every time it changes:

      set(show(complete)).
      prove( th1, []).

Since the recursive structure of qs does not co-incide with that of its parameter type list, we cannot use ordinary induction on list to prove this theorem, but have to use computational induction (i.e. the lazy induction command described in section 7.4.17) on qs after convincing ourselves that qs fulfils the requirements for the use of this command:

      lazy induction(qs).

After which Seduct displays^{19}:

         % Now proving:  "th1 lazy 1".
      Antecedent:

19To avoid drowning the reader in insignificant information, we will, in general, only show the relevant part of what is displayed by Seduct.

Succedent:
 (1)  ordered([])

Since the succedent is matched by the left-hand side of a definition, we simplify it with

expand all.

and prove the resulting trivial sequent with

go.

Now, the second sequent resulting from the lazy induction(qs) command is displayed:

Antecedent:
 (1)  ordered(qs small part(c1,c2))
 (2)  ordered(qs big part(c1,c2))
Succedent:
 (1)  ordered(qs small part(c1,c2) * c1 @ qs big part(c1,c2))

Again, we try using

expand all.

but this time it leaves the sequent unchanged since no formula is matched by the left-hand side of a definition. A closer look at the succedent makes it clear that what is needed is a rule for the distribution of ordered over *. In order to conveniently formulate this rule, we also need two more infix operators and end up with the following:

begin(declare).
   (>>=): [ element, list] -> bool.
   (==<<): [ list, list] -> bool.
end(declare).
op( 25, xfx, >>=).
op( 26, xfx, ==<<).
begin(definitions).
   '>>= 1': forall( x: element, x >>= []).
   '>>= 2': forall( [ x: element, y: element, l: list],
      x >>= y @ l <--> x >= y & x >>= l).
   '==<< 1': forall( l: list, [] ==<< l).
   '==<< 2': forall( [ x: element, l1: list, l2: list],
      x @ l1 ==<< l2 <--> x =<< l2 & l1 ==<< l2).
end(definitions).
goal( lemma 1: forall( [ l1: list, l2: list],
      ordered(l1 * l2) <--> ordered(l1) & ordered(l2) & l1 ==<< l2)).

We now try to prove lemma 1 by induction over l1:

prove( lemma 1, []).
induction(l1).

The base case is easily proven by

expand all.
go.

and the induction step is also expanded using

expand all.

to give:

Antecedent:

 (1)  forall( [ l2: list],
   ordered(c6 * l2) <--> ordered(c6) & ordered(l2) & c6 ==<< l2)
Succedent:
 (1)  forall( [ l2: list],
   c5 =<< c6 * l2 & ordered(c6) & ordered(l2) & c6 ==<< l2 <-->
      (c5 =<< c6 & ordered(c6)) & ordered(l2) & c5 =<< l2 & c6 ==<< l2)

This formula is unpleasantly complicated, so we reduce it, using:

skolemize.
beta normalize.

Since the succedent contains nine conjuncts, we should expect beta normalize to generate nine cases, but several of these are so trivial that beta normalize dismisses them automatically. The first one for us to worry about is:

Antecedent:
 (1)  ordered(c7)
 (2)  c6 ==<< c7
 (3)  ordered(c6)
 (4)  c5 =<< c6 * c7
 (5)  forall( [ l2: list], ordered(c6 * l2) <--> ordered(c6) & ordered(l2) & c6 ==<< l2)
Succedent:
 (1)  c5 =<< c6

which would be easy to prove if we had a rule for the distribution of =<< over *.

Therefore, we formulate such a rule:

goal( lemma 2: forall( [ x: element, l1: list, l2: list],
   x =<< l1 * l2 <--> x =<< l1 & x =<< l2)).

We have formulated the lemma as an equivalence although an implication would seem to suffice. There are two reasons for this: one is that, as for ord2, we want this lemma to be usable for expansion, another that we expect to need the implication in the other direction later – and it is often easier to prove one equivalence than two implications.

We prove lemma 2 by means of induction over l1 leaving the base case to Seduct in the usual way:

prove( lemma 2, []).
induction(l1).
expand all.
go.

ending up with an induction step:

Antecedent:
 (1)  forall([ x: element, l2: list], x =<< c9 * l2 <--> x =<< c9 & x =<< l2)
Succedent:
 (1)  forall( [ x: element, l2: list], x =<< c8 @ c9 * l2 <--> x =<< c8 @ c9 & x =<< l2)

which is simple enough to be proven by

expand all.
go.

We have now finished proving the correctness of lemma 2 and, since we want it to be used by expand all, instruct Seduct to treat it as a definition:

use as definition(lemma 2).

and are now able to complete the proof of the first beta normalize case of lemma 1 by

expand all.
go.

The second beta normalize case:

Antecedent:
(1)  ordered(c7)
(2)  c6 ==<< c7
(3)  ordered(c6)
(4)  c5 =<< c6 * c7
(5)  forall( [ l2: list], ordered(c6 * l2) <--> ordered(c6) & ordered(l2) & c6 ==<< l2)
Succedent:
(1)  c5 =<< c7

can be handled the same way:

expand all.
go.

and the third:

Antecedent:
(1)  c5 =<< c7
(2)  c6 ==<< c7
(3)  ordered(c7)
(4)  c5 =<< c6
(5)  ordered(c6)
(6)  forall( [ l2: list], ordered(c6 * l2) <--> ordered(c6) & ordered(l2) & c6 ==<< l2)
Succedent:
(1)  c5 =<< c6 * c7

likewise:

expand all.
go.

The fact that all three sequents generated by the beta normalize command could be handled in the same simple manner once lemma 2 had been defined indicates that the use of this command was not necessary in the first place – we will remember this for later.

This concludes the proof of lemma 1 and, since we want to use this lemma for expansion, we instruct Seduct to treat it as a definition:

use as definition(lemma 1).

and expand the current sequent (we are now back in the proof of the original theorem th1):

expand all.

getting:

Antecedent:
(1)  ordered(qs small part(c1,c2))
(2)  ordered(qs big part(c1,c2))
Succedent:
(1)  c1 =<< qs big part(c1,c2) & qs small part(c1,c2) ==<< c1 @ qs big part(c1,c2)

At this point there are several possibilities. We choose to define the following lemmata:

goal( lemma 3: forall( [ x: element, l: list], x =<< qs l <--> x =<< l)).
goal( lemma 4: forall( [ x: element, l: list], x >>= qs l <--> x >>= l)).

again formulating them as equivalences so that they can be used by expand all.

We start proving lemma 3 which, like th1, because of the application of qs lends itself to a proof by lazy induction. Here, the base case is so simple that not even expand all is needed for its proof:

prove( lemma 3, []).
lazy induction(qs).
go.

After an

expand all.

the induction step looks as follows:

Antecedent:
 (1)  c18 =<< qs small part(c14,c15) <--> c18 =<< small part(c14,c15)
 (2)  c18 =<< qs big part(c14,c15) <--> c18 =<< big part(c14,c15)
Succedent:
 (1)  c18 =<< small part(c14,c15) & c18 =< c14 & c18 =<< big part(c14,c15) <-->
   c18 =< c14 & c18 =<< c15

which can easily be proven using the following lemma:

goal( lemma 5: forall( [ x: element, y: element, l: list],
   x =<< small part(y,l) & x =<< big part(y,l) <--> x =<< l)).

which we continue to prove in the usual manner:

prove( lemma 5, []).
induction(l).
expand all.
go.
expand all.

getting the following expanded induction step:

Antecedent:
 (1)  forall( [ x: element, y: element],
   x =<< small part(y,c21) & x =<< big part(y,c21) <--> x =<< c21)
Succedent:
 (1)  forall( [ x: element, y: element],
   if( c20 < y, x =< c20 & x =<< small part(y,c21), x =<< small part(y,c21)) &
      if( c20 >= y, x =< c20 & x =<< big part(y,c21),
         x =<< big part(y,c21)) <--> x =< c20 & x =<< c21)

To simplify the structure of the succedent, we split up the ifs after first performing the for the split if necessary skolemization:

skolemize.
split if.

The first resulting sequent:

Antecedent:

       (1)  c23 =< c20
       (2)  c20 < c23
       (3)  forall([ x: element,y: element],
         x =<< small part(y,c21) & x =<< big part(y,c21) <--> x =<< c21)
      Succedent:
       (1)  (c22 =< c20 & c22 =<< small part(c23,c21)) &
         c22 =< c20 & c22 =<< big part(c23,c21) <--> c22 =< c20 & c22 =<< c21

and the other three generated by the split if command are so simple that each can be proven without further interaction:

      go.
      go.
      go.
      go.

completing the proof of lemma 5. Obviously, the sequent from before the split if command could also have been proven by simply issuing a go command – we will take advantage this knowledge shortly.

Since lemma 5 does not have the form of a definition, we add it as a theorem to be used when proving the remaining sequent of lemma 3:

      go([lemma 5]).

which completes the proof of lemma 3.

For lemma 4, we would expect the proof to be equivalent to that of lemma 3. So let us first define the equivalent

of lemma 5:
      goal( lemma 6: forall( [ x: element, y: element, l: list],
         x >>= small part(y,l) & x >>= big part(y,l) <--> x >>= l)).

The Seduct commands used for the proof of lemma 6 are, of course, the same as for lemma 5, and are of a very general nature, so it seems advantageous to define a macro to perform that kind of proofs:

      macro( symbolic execution, goal, var, theory).
         prove( goal, theory).
           induction(var).
              expand all.
              go.
              expand all.
              go.
      end(symbolic execution).

Although, no additional theory was needed for the proof of lemma 5 (i.e. the theory argument for the prove command was empty), we have generalized the macro by adding such an argument.

Using this macro, we are now able to prove lemma 6:

      symbolic execution( lemma 6, l, []).

It would likewise seem advantageous to define an equivalent macro using lazy induction to perform the proof of lemma 4 which we expect to be the same as for lemma 3. This macro has not been included here since it is not able to complete the proof with the current set of lemmata, and we will have to perform it manually to see what is missing.

The first part of the proof looks the usual way:

      prove( lemma 4, []).
      lazy induction(qs).
      go.

expand all.

but the resulting sequent

Antecedent:
 (1)  c34 >>= qs small part(c30,c31) <--> c34 >>= small part(c30,c31)
 (2)  c34 >>= qs big part(c30,c31) <--> c34 >>= big part(c30,c31)
Succedent:
 (1)  c34 >>= qs small part(c30,c31) * c30 @ qs big part(c30,c31) <-->
   c34 >= c30 & c34 >>= c31

cannot be proven by go([lemma 6]) as was expected.

A closer inspection of the sequent shows that a lemma distributing >>= over * (equivalent to the previously defined lemma 2 distributing =<< over *) is missing:

goal( lemma 7: forall( [ x: element, l1: list, l2: list],
   x >>= l1 * l2 <--> x >>= l1 & x >>= l2)).

Knowing from the proof of lemma 2 that this proof has the by now familiar structure, we use the macro symbolic execution for the proof:

symbolic execution( lemma 7, l1, []).

We are now able to expand the remaining sequent of lemma 4 and complete the proof of this lemma:

use as definition(lemma 7).
expand all.
go([lemma 6]).

Now back in the proof of the original theorem th1, we also want to use lemma 3 and lemma 4 as were they definitions:

use as definition(lemma 3).
use as definition(lemma 4).

and expand the current sequent:

expand all.

to get:

Antecedent:
 (1)  ordered(qs small part(c1,c2))
 (2)  ordered(qs big part(c1,c2))
Succedent:
 (1)  c1 =<< big part(c1,c2) & qs small part(c1,c2) ==<< c1 @ qs big part(c1,c2)

Here, a lemma like:

goal( lemma 8: forall( [ x: element, l: list], x >>= small part(x,l))).

would come in handy, and, because it looks very simple, we try to prove it with the symbolic execution macro:

symbolic execution( lemma 8, l, []).

which succeeds. The equivalent

goal(lemma 9: forall( [ x: element, l: list], x =<< big part(x,l))).

is proven in the same manner:

symbolic execution( lemma 9, l, []).

Using both lemmata as definitions, we can expand the current sequent:

use as definition(lemma 8).
use as definition(lemma 9).
expand all.

to get:

Antecedent:
 (1)  ordered(qs small part(c1,c2))
 (2)  ordered(qs big part(c1,c2))
Succedent:
 (1)  qs small part(c1,c2) ==<< c1 @ qs big part(c1,c2)

In this sequent, we would like to replace application of ==<< with applications of =<< and >>= for which we already have a number of lemmata. This can be accomplished by the following lemma:

goal( lemma 10: forall( [ x: element, l1: list, l2: list],
   x >>= l1 & x =<< l2 -> l1 ==<< l2)).

This lemma cannot be formulated so as to have the form of a definition, since the reverse implication is not true^{20}. As we do not expect the symbolic execution macro to be able to prove this lemma, we start proving it manually in the usual way:

prove( lemma 10, []).
induction(l1).
expand all.
go.
expand all.

ending up with the following expanded induction step:

Antecedent:
 (1)  forall( [ x: element, l2: list], x >>= c47 & x =<< l2 -> c47 ==<< l2)
Succedent:
 (1)  forall( [ x: element, l2: list],
   (x >= c46 & x >>= c47) & x =<< l2 -> c46 =<< l2 & c47 ==<< l2)

Here, all that is missing is

goal( lemma 11: forall( [ x: element, y: element, l: list],
   x =< y & y =<< l -> x =<< l)).

which can be proven by our trusted macro:

symbolic execution( lemma 11, l, []).

Using this lemma we can finish the proof of lemma 10:

go([lemma 11]).

and are now ready to finish the proof of th1.

Since lemma 10 does not have the form of a definition, we cannot simply use expand all. On the other hand, lemma 10 does not suffice to prove the current sequent, so we have to consider which lemmata are needed for the go command to be able to complete the proof. We add these to the antecedent:

add( [ lemma 3, lemma 4, lemma 8, lemma 9, lemma 10]).

20Quantifying x existentially would make the reverse implication true, but definitions cannot be existentially quantified.

Unfortunately, go is still not able to complete the proof, so in order to figure out what is missing, we issue the command:

      crunch.

which generates the following sequent:

      Antecedent:

⋮

      Succedent:
       (1)  meta(72) =<< meta(74)
       (2)  qs small part(c1,c2) ==<< c1 @ qs big part(c1,c2)

indicating that we need a lemma which is dual to the axiom ==<< 2:

      goal( lemma 12: forall( [ x: element, l1: list, l2: list],
         l1 ==<< x @ l2 <--> x >>= l1 & l1 ==<< l2)).

which can be proven in the usual way and used as a definition:

      symbolic execution( lemma 12, l1, []).
      use as definition(lemma 12).

To avoid wasting time expanding a lot of unnecessary formulae, we select the interesting formula from the succedent and expand it:

      select( [], [2]).
      expand all.

Using the same additional theorems as above^{21}, we are now able to complete the proof:

      go( [ lemma 3, lemma 4, lemma 8, lemma 9, lemma 10]).

Now, we ought to show that the conditions for the use of the lazy induction command are indeed fulfilled, and and to prove that the elements of the sorted list are the same as those of the original list. For the former task which cannot be performed by Seduct, it is recommended to use a tool like CCC (cf. [10]) which can also ensure the consistency of the specification. The latter task for which Seduct is well suited is left to the reader.

4.2.3 Presenting the Proof

If we had implicitly believed whatever a program tells us, there would be no more to do. Being soundly sceptical, however, we want to at least present the proof in such a way that a human being will have a chance to understand it.

To simplify the structure of the proof, we move anything we can (e.g. declarations, definitions and other proofs) out of each proof, get rid of unnecessary commands like the crunch above, merge all declarations into into one declarations section, etc. Working inside out, we move ‘clean’ proofs, declarations etc. out of other proofs. Finally, we present the proofs in some reasonable order, and see if we could not use macros to further simplify the presentation of the entire proof. For the above proof, we have come up with the following:

      begin(declare).
         ([]): list.
         (@): [ element, list] -> list.
         (*): [ list, list] -> list.
         small part: [ element, list] -> list.
         big part: [ element, list] -> list.
         qs: [list] -> list.

21These additional theorems could, of course, also have been selected from the shadow sequent, but using the same theory definition as above is easier.

ordered: [list] -> bool.
(=<<): [ element, list] -> bool.
(>>=): [ element, list] -> bool.
(==<<): [ list, list] -> bool.
end(declare).
op( 10, xfy, @).
op( 15, xfy, *).
op( 10, fy, qs).
op( 25, xfx, =<<).
op( 25, xfx, >>=).
op( 26, xfx, ==<<).
linear ordered(element).
freely generated( list, [ ([]), (@)]).
begin(definitions).
append1: forall( l: list, [] * l = l).
append2: forall( [ x: element, l: list, k: list], x@l * k = x @ (l * k)).
s1: forall( x: element, small part(x,[]) = []).
s2: forall( [ x: element, y: element, l: list],
   small part(x,y@l) = if( y < x, y @ small part(x,l), small part(x,l))).
b1: forall( x: element, big part(x,[]) = []).
b2: forall( [ x: element, y: element, l: list],
   big part(x,y@l) = if( y >= x, y @ big part(x,l), big part(x,l))).
qs1: qs [] = [].
qs2: forall( [ x: element, l: list],
   qs x@l = qs small part(x,l) * x @ qs big part(x,l)).
'=<< 1': forall( x: element, x =<< []).
'=<< 2': forall( [ x: element, y: element, l: list],
   x =<< y@l <--> x =< y & x =<< l).
'>>= 1': forall( x: element, x >>= []).
'>>= 2': forall( [ x: element, y: element, l: list],
   x >>= y@l <--> x >= y & x >>= l).
'==<< 1': forall( l: list, [] ==<< l).
'==<< 2': forall( [ x: element, l1: list, l2: list],
   x@l1 ==<< l2 <--> x =<< l2 & l1 ==<< l2).
ord1: ordered([]).
ord2: forall( [ x: element, l: list], ordered(x@l) <--> x =<< l & ordered(l)).
end(definitions).
begin(goals).
lemma 2: forall( [ x: element, l1: list, l2: list],
   x =<< l1 * l2 <--> x =<< l1 & x =<< l2).
lemma 7: forall( [ x: element, l1: list, l2: list],
   x >>= l1 * l2 <--> x >>= l1 & x >>= l2).
lemma 1: forall( [ l1: list, l2: list],
   ordered(l1 * l2) <--> ordered(l1) & ordered(l2) & l1 ==<< l2).
lemma 8: forall( [ x: element, l: list], x >>= small part(x,l)).
lemma 9: forall( [ x: element, l: list], x =<< big part(x,l)).
lemma 11: forall( [ x: element, y: element, l: list], x =< y & y =<< l -> x =<< l).
lemma 10: forall( [ x: element, l1: list, l2: list],
   x >>= l1 & x =<< l2 -> l1 ==<< l2).
lemma 12: forall( [ x: element, l1: list, l2: list],

      l1 ==<< x @ l2 <--> x >>= l1 & l1 ==<< l2).
   lemma 5: forall( [ x: element, y: element, l: list],
      x =<< small part(y,l) & x =<< big part(y,l) <--> x =<< l).
   lemma 6: forall( [ x: element, y: element, l: list],
      x >>= small part(y,l) & x >>= big part(y,l) <--> x >>= l).
   lemma 3: forall( [ x: element, l: list], x =<< qs l <--> x =<< l).
   lemma 4: forall( [ x: element, l: list], x >>= qs l <--> x >>= l).
   th1: forall( [ l: list], ordered(qs l)).
end(goals).
macro( symbolic execution, goal, var, theory).
   prove( goal, theory).
      induction(var).
         expand all.
         go.
         expand all.
         go.
   use as definition(goal).
end(symbolic execution).
macro( lazy prove, goal, function, theory).
   prove( goal, theory).
      lazy induction(function).
         expand all.
         go.
         expand all.
         go.
   use as definition(goal).
end(lazy prove).
symbolic execution( lemma 2, l1, []).
symbolic execution( lemma 7, l1, []).
symbolic execution( lemma 1, l1, []).
symbolic execution( lemma 8, l, []).
symbolic execution( lemma 9, l, []).
symbolic execution( lemma 11, l, []).
symbolic execution( lemma 10, l1, [lemma 11]).
symbolic execution( lemma 12, l1, []).
symbolic execution( lemma 5, l, []).
symbolic execution( lemma 6, l, []).
lazy prove( lemma 3, qs, [lemma 5]).
lazy prove( lemma 4, qs, [lemma 6]).
lazy prove( th1, qs, [ lemma 3, lemma 4, lemma 8, lemma 9, lemma 10]).

We have enhanced the symbolic execution macro to include a use as definition command, which is safe since the expand all command dismisses all definitions that do not have the proper form. The lazy prove macro is

the same as symbolic execution except that it uses lazy induction instead of induction.

Apart from grouping of declarations etc., reordering of everything, and the use of macros, nothing has been changed from the proof described in the previous section. To make the correspondence clear, even the names of the lemmata have been left unchanged although they are not very well suited to the current ordering of the lemmata.

Having finished proving the correctness of a second algorithm, we can now lean back an enjoy the drink we mixed after proving the correctness of the insertion sort algorithm.

5 The Sequent Calculus

In order to understand what is going on behind the go command the user has to get at least a rough idea of the proof methods employed by Seduct to prove a many–sorted first–order formula. Therefore we suggest that even readers who feel a little bit uneasy with formal methods should at least read the first subsection describing the notion of a formal proof and glance over the second subsection discussing the sequent calculus. Otherwise they will not be able to interact with Seduct when a proof goes wrong. The next section will describe the rewriting techniques employed.

5.1 What Constitutes a Formal Proof?

Seduct is intended to prove theorems. While humans are able to do proofs in an informal setting, computers are only capable of manipulating syntactic structures. Therefore there has to be a formal counterpart of the intuitive notion of a proof. We call this counterpart a formal proof. The main ingredients of a formal proof are

• Axioms and

• Rules.

Axioms are formulas which are considered to be true and therefore need no further proof. A rule is a pair consisting of a formula called the conclusion and a list of formulas called the premisses of the rule. If the rule is given as

( Conclusion, [ Premise_{1}, ⋯, Premise_{n} ] ) then it is intended to express the fact that to prove the formula Conclusion it is sufficient to prove the formulae Premise_{i} for all i ∈ {1, ⋯, n}. Normally, rules are not displayed in the way we have done it above but rather two dimensionally. The general form of a rule then looks like the following:

\frac{Premise_{1} ⋯ Premise_{n}}{Conclusion} .

The intended meaning of a rule is that in order to prove the conclusion it is sufficient to prove all premisses.

A collection of axioms and rules constitutes a calculus. To keep things from getting too abstract, we will give an example. The calculus we are going to construct in this subsection will have only one axiom:^{22}

A -> A.

There will be two rules in our calculus. The first is very simple and has one premise:

\frac{A -> B}{¬¬A -> B} .

The second one has two premisses.

\frac{B -> C ¬A -> C}{(A -> B) -> C}

The calculus so defined will only be used in this subsection and is given purely for illustrative purposes.

Having defined the notions of axioms and rules we can proceed to define proofs. A proof is constructed from the axioms using only the rules of the calculus. The set of formal proofs can be defined inductively as a set of strings in the following way:

1. If Axiom is an axiom, then the string pr( Axiom )

is a formal proof of the formula Axiom.

22Taken literally this is not an axiom but rather an axiom scheme describing a set of axioms because A is used as a placeholder for an arbitrary formula.

2. If

\frac{Premise_{1} ⋯ Premise_{n}}{Conclusion}

is a rule, and if furthermore for all i ∈ {1, ⋯, n} the term Proof_{i} is a formal proof of the formula Premise_{i}, then the string

pr( Conclusion , [ Proof_{1}, ⋯, Proof_{n} ] )

is a formal proof of the formula Conclusion.

This is the way proofs are represented in a computer. For a computer, this representation is well suited. However for humans a graphical, two dimensional representation is much more convenient. We depict a proof as a tree, whose nodes are marked with formulas such that the following holds:

1. All leafs are marked with axioms.

2. If an inner node is marked with a formula F, and if this node has got n sons which are labeled with the formulas P_{1}, P_{2}, ⋯, P_{n} respectively, then the calculus used has to contain a rule of the form

\frac{P_{1} P_{2} ⋯ P_{n}}{F} .

To clarify matters, we give an example of a proof. Suppose p is a nullary predicate symbol, then the following tree represents a proof of the formula (¬p -> p) -> p:

                                    \frac{p -> p      \frac{p -> p}{¬¬p -> p}}{(¬p -> p) -> p} .

After having seen what a proof is, we have to solve the question of how to find a proof for a given conjecture. One method would be to start from axioms and apply rules in some systematic fashion thereby enumerating the set of theorems. However, this method is much too inefficient to be of any practical use. In fact one proceeds the other way round. When searching for a proof, we try to work backwards. That is, given a formula to be proved, the method employed by Seduct is to look for a rule which can produce the formula in question when given the right hypotheses as premisses. Having found such a rule, the task then is to prove the premisses. This can be done by either noting that a premise is an axiom or by applying the same method recursively to the premise. The procedure described above is also known as backward chaining. Because of its importance, we give an example of this procedure in a later section.

5.2 A Cut Free Sequent Calculus

In the rest of this section we are going to describe a cut free sequent calculus which is complete for first order logic without equality. We will presuppose some knowledge of first order logic, as it is exposed for example in the books of Enderton [4], Gallier [5] or Smullyan [11].

The calculus we will develop does not work with formulas but uses sequents instead. For a start, we define this notion: Sequents are pairs of finite multisets^{23} of formulas. If we have

Γ = [A_{1}, …, A_{m}] and Δ = [B_{1}, …, B_{n}],

then we regard the sequent Γ ⊢ Δ as representing the formula

A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}.

Notation: In this section we will use the following notation: Upper case greek laters (e.g., Γ, Δ, …) will be used to designate finite multisets of formulas. Single formulas will be written using upper case latin letters in math style (e.g., A, B, …, F, G, …). Terms will be denoted by lower case latin letters printed in math style (e.g., a, b, c, …, r, s, t ). Because there is no easy way to print the symbols ^and & in the math mode of LaTEX, we change our previous conventions on notation slightly and use from now on the following conventions:

23Multisets are very much like sets, the only difference being that they may contain an element several times. To be able to distinguish sets and multisets we use the brackets “[” and “]” for multisets, while the curly brackets “{” and “}” are reserved for sets.

1. The negation of a formula A is now written as ¬A instead of ^A.

2. The conjunction of two formulas A and B is now written as A ∧ B instead of A & B.

3. The disjunction of two formulas A and B is now written as A ∨ B instead of A v B.

4. The implication of two formulas A and B is now written as A → B instead of A -> B.

5. The equivalence of two formulas A and B is now written as A ↔ B instead of A <--> B.

6. The universal quantification of formula A with respect to a variable x of sort s is now written as ∀ x:s.A instead of forall(x:s,A). If the sort s is either clear from the context or else unimportant we will just write ∀ x.A.

The shorthand notation forall([x_{1}:s_{1} ⋯ x_{n}:s_{n}],A) will be replaced by ∀ x_{1}: s_{1} ⋯, x_{n}: s_{n}.A. Again, sorts may be omitted. Furthermore, an arrow notation is sometimes used. Then the formula above is written as ∀x⃗.A.

7. The existential quantification of formula A with respect to a variable x of sort s is now written as ∃ x:s.A instead of exists(x:s,A). If the sort s is either clear from the context or else unimportant we will just write ∃ x.A.

The shorthand notation exists([x_{1}:s_{1} ⋯ x_{n}:s_{n}],A) will be replaced by ∃ x_{1} : s_{1} ⋯, x_{n}: s_{n}.A where sorts may be omitted. As in the case of the universal quantifier, an arrow notation may be used.

If Γ is a finite multiset of formulas and A is a formula, we will write Γ, A as an abbreviation for the multiset Γ ∪ [A].

If A is a formula, t a term and x a variable, then A[x ← t] denotes the formula obtained from A by replacing every occurrence of x by t. When performing this operation one has to be sure that no variables occurring in t are bound afterwards. For example, take the formula A defined as (we use the symbol “≡” to denote literal equality)

A ≡ ∃y(x + 1 = y),

which is obviously true when interpreted in the structure of the natural numbers. However, substituting the term y^{2} for x in the formula A we would get

A[x ← y^{2}] ≡ ∃y(y^{2} + 1 = y).

If we had defined the formula A[x ← y^{2}] this way, then this formula would no longer be true in the structure of the natural numbers. To avoid situations like the one described above bound variables are renamed before substitutions. This is necessary to prevent variable clashes. With this agreement we have

A[x ← y^{2}] ≡ ∃z(y^{2} + 1 = z).

5.3 The Preprocessing

To start with, we have to do some preprocessing of the formulas in order to get rid of certain defined constructs. Presently the only defined construct eliminated is the if–operator appearing on the term level. As an example, consider the if operator in the following definition of the function min:

min(x, y) = if( x ≤ y, x, y)

This if–operator can be eliminated to yield the equivalent formula

if( x ≤ y, min(x, y) = x, min(x, y) = y ).

Of course, the last formula still contains an if–operator. But this if–operator is different from the if–operator occuring in the first formula because it takes subformulas rather than terms as its second and third arguments.

Therefore this last version of the if–operator will present no problem in the sequent calculus developed later on since it can be interpreted as a propositional symbol just like ¬, ∧, or →.^{24}

To eliminate non–propositional if–operators we need two transformation rules for formulas. The first transformation rule works entirely on terms and has got the form:

f( s_{1}, ⋯, s_{i−1}, if( B, t^{(1)}, t^{(2)} ), s_{i+1}, ⋯, s_{n} ) =
if( B, f( s_{1}, ⋯, s_{i−1}, t^{(1)}, s_{i+1}, ⋯, s_{n}), f( s_{1}, ⋯, s_{i−1}, t^{(2)}, s_{i+1}, ⋯, s_{n}) )

The f occurring in this transformation rule stands for an arbitrary function symbol. Because the formula above is rather long and therefore difficult to understand, we present a simplified version of it, which however is less precise:

f( ⋯, if( B, t^{(1)}, t^{(2)} ), ⋯, ) = if( B, f( ⋯, t^{(1)}, ⋯, ), f( ⋯, t^{(2)}, ⋯, ) )

This transformation rules moves the if–operators from subterms to terms. It does not eliminate them. This is achieved by the second transformation rule. It is:

p( ⋯, if( B, t^{(1)}, t^{(2)} ), ⋯, ) ↔ if( B, p( ⋯, t^{(1)}, ⋯, ), p( ⋯, t^{(2)}, ⋯, ) )

Here the symbol p stands for an arbitrary predicate symbol, including the equality symbol = or any of the inequality symbols ≤, ≥, <, or >.

5.4 The Axioms

The sequent calculus we have implemented in Seduct contains four different axiom schemes:

1. Γ, false ⊢ Δ is an axiom.

2. Γ ⊢ Δ, true is an axiom.

3. Γ, ∀x_{1}, ⋯, x_{n}.P ⊢ Δ, ∃x_{1}, ⋯, x_{n}.Q is an axiom provided that P and Q are unifiable. (Here P and Q are metavariables ranging over prime formulas.)

4. Γ ⊢ Δ, ∃x_{1}, ⋯, x_{n}.P = Q is an axiom provided that P and Q are unifiable. (Again, P and Q are metavariables ranging over prime formulas.)

Following Smullyan [11] we divide the rules into α, β, γ and δ rules. For reasons of efficiency we have added some rules to the class of the α and the δ rules. To deal with inequations efficiently we need a further type of rules which we have called ι rules. We now describe each of these classes of rules in turn.

5.5 The α Rules

The α rules are propositional rules which cause no branching in the proof tree. Traditionally, the following α rules are used:

1. Introduction of ¬ in the antecedent:

\frac{Γ ⊢ Δ, A}{Γ, ¬A ⊢ Δ}(¬A)

2. Introduction of ¬ in the succedent:

\frac{Γ, A ⊢ Δ}{Γ ⊢ Δ, ¬A}(¬S)

24As a matter of fact, the if–operator on the propositional level can be defined as:

if(p, q, r) ↔ (p → q) ∧ (¬p → r).

3. Introduction of ∧ in the antecedent:

\frac{Γ, A, B ⊢ Δ}{Γ, A ∧ B ⊢ Δ}(∧A)

4. Introduction of ∨ in the succedent:

\frac{Γ ⊢ Δ, A, B}{Γ ⊢ Δ, A ∨ B} (∨S)

5. Introduction of → in the succedent:

\frac{Γ, A ⊢ Δ, B}{Γ ⊢ Δ, A → B} (→S)

In addition to these rules we use five other rules which describe distribution relations between the quantifiers ∀, ∃ and the propositional symbols ∧, ∨, ¬ and →. We list these rules below:

1. Introduction of ¬ in the antecent under an universal quantifier:

\frac{Γ ⊢ Δ, ∃x⃗.A}{Γ, ∀x⃗.¬A ⊢ Δ}(∀¬A)

2. Introduction of ¬ in the succedent under an existential quantifier:

\frac{Γ, ∀x⃗.A ⊢ Δ}{Γ ⊢ Δ, ∃x⃗.¬A}(∃¬S)

3. Introduction of ∧ in the antecent under an universal quantifier:

\frac{Γ, ∀x⃗.A, ∀x⃗.B ⊢ Δ}{Γ, ∀x⃗.A ∧ B ⊢ Δ}(∀∧A)

4. Introduction of ∨ in the succedent under an existential quantifier:

\frac{Γ ⊢ Δ, ∃x⃗.A, ∃x⃗.B}{Γ ⊢ Δ, ∃x⃗.A ∨ B} (∃∨S)

5. Introduction of → in the succedent under an existential quantifier:

\frac{Γ, ∀x⃗.A ⊢ Δ, ∃x⃗.B}{Γ ⊢ Δ, ∃x⃗.A → B} (∃→S)

The reason for adding these rules will become clear when we discuss the γ rules.

5.6 The β Rules

The β rules are the rules which are responsible for the branching of proof trees.

1. Introduction of ∧ in the succedent:

\frac{Γ ⊢ Δ, A Γ ⊢ Δ, B}{Γ ⊢ Δ, A ∧ B} (∧S)

2. Introduction of ∨ in the antecedent:

\frac{Γ, A ⊢ Δ Γ, B ⊢ Δ}{Γ, A ∨ B ⊢ Δ}(∨A)

3. Introduction of → in the antecedent:

\frac{Γ ⊢ Δ, A Γ, B ⊢ Δ}{Γ, A → B ⊢ Δ}(→A)

4. Introduction of ↔ in the antecedent:

\frac{Γ, A, B ⊢ Δ Γ ⊢ Δ, A, B}{Γ, A ↔ B ⊢ Δ} (↔A)

5. Introduction of ↔ in the succedent:

\frac{Γ, A ⊢ Δ, B Γ, B ⊢ Δ, A}{Γ ⊢ Δ, A ↔ B}(↔S)

The rules described so far are the classical β–rules. But we need two additional β–rules to deal with the if– operator. These rules are as follows:

6. Introduction of if in the antecedent:

\frac{Γ, B, F_{1} ⊢ Δ Γ, F_{2} ⊢ Δ, B}{Γ, if(B, F_{1}, F_{2}) ⊢ Δ} (ifA)

7. Introduction of if in the succcedent:

\frac{Γ, B ⊢ Δ, F_{1} Γ ⊢ Δ, B, F_{2}}{Γ ⊢ Δ, if(B, F_{1}, F_{2})} (ifS)

5.7 The γ Rules

There are only two γ rules:

1. Introduction of ∀ in the antecedent:

\frac{Γ, P [x ← t] ⊢ Δ}{Γ, ∀x.P ⊢ Δ}(∀A)

2. Introduction of ∃ in the succedent:

\frac{Γ ⊢ Δ, P [x ← t]}{Γ ⊢ Δ, ∃x.P}(∃S)

You will notice that the t appearing in these rules is printed in boldface. This is no accident but rather reflects the fact that t is a metavariable and not a term. At this point, two questions arise: What is a metavariable and why do we need it? To answer the first question, a metavariable is just an object of our meta language. It does not denote an object of the domain of discourse, but rather a syntactic object of our object language, that is to say the formal language we use as input for Seduct. It is intended to be instantiated later by a term of our object language. To understand why we need metavariables, consider a version of the γ rules using no metavariables. They would look like the following:

1. Introduction of ∀ in the antecedent:

\frac{Γ, P [x ← t] ⊢ Δ}{Γ, ∀x.P ⊢ Δ}(∀A)

2. Introduction of ∃ in the succedent:

\frac{Γ ⊢ Δ, P [x ← t]}{Γ ⊢ Δ, ∃x.P}(∃S)

Here t is just a normal term to be substituted for x. But now there is a problem. We have already pointed out that Seduct works backwards when searching for a proof. That is, given a sequent to be proved, Seduct tries to find a rule which can produce this sequent when starting with the right hypotheses. After that the sequent to be proved is replaced by the hypotheses. In order for this to work we have to be able to compute the form of the sequents used as premisses. This imposes certain constraints on the rules to be used. For example a rule^{25} like

\frac{Γ ⊢ Δ, C Γ, C ⊢ Δ}{Γ ⊢ Δ} (cut)

can not be used, because starting from the sequent Γ ⊢ Δ, how should we compute the formula C? The problem is similar when we use the version of the γ rules just given. How should we compute the term t? At least at this stage of the proof there is no obvious way to determine t. Therefore it is best to postpone the decision of how t should be chosen by introducing a metavariable instead. Of course, at some stage this metavariable has to be instantiated, because otherwise we would not get a formal proof, since a formal proof is constructed solely from formulas and these do not contain any metavariables. How then do these metavariables get instantiated? The answer is simple: Consider a sequence of the form

Γ, ∀x_{1}, ⋯, x_{n}.A ⊢ Δ, ∃x_{1}, ⋯, x_{n}.B.

If we are able to unify A and B, this is an axiom. If A and B contain metavariables, then now it is the right time to instantiate them. If we can instantiate them in a way such that afterwards A and B become unifiable, we perform this instantiation. (From an implementational point of view this is a straightforward strategy because we can use the unification algorithm to do both the instantiation of the metavariable and the checking whether A and B are unifiable in one step.)

There is one very important point in which the γ rules differ from all other rules. To make this point, we have to introduce the notion of analytical rules.

Definition 1 (Analytical Rules) A rule is analytical if the truth of its conclusion implies the truth of all of its premisses.

The importance of analytical rules stems from the fact that while searching for a proof we can apply them backwards without having to fear of ending up with premisses that are no longer provable. In other words, if we are proving a sequent Γ ⊢ Δ and apply an analytical rule to get a new sequent Γ′ ⊢ Δ′, then there will be a proof for this new sequent provided there was a proof for the old sequent. Now comes the important point:

The γ rules are not analytical.

To illustrate the fact that γ rules are not analytical, consider the sequent ∀x.p(x) ⊢ ∀x.p(x). This sequent is certainly true. Let us try to prove it using the γ rule (∀A). This atempt results in the partial^{26} proof

p(t) ⊢ ∀x.p(x)
∀x.p(x) ⊢ ∀x.p(x)

where t is a metavariable which has to be instantiated properly. Now, how could the metavariable t be possibly instantiated to get a proof of the sequent p(t) ⊢ ∀x.p(x)? The answer is quite simple: There can be no instantiation for t to make this sequent provable, because there is no instantiation to make this sequent valid.

There is one other problem, which is connected with the fact that γ rules are not analytical. We illustrate it with a simple example. Suppose we wanted to prove the sequent

∀x.p(x) ⊢ p(a) ∧ p(b),

where a and b are constants of the appropiate sort. Suppose we started the proof with the application of the γ rule “introduction of ∀ in the antecedent”. This would leave us with the sequent

p(t) ⊢ p(a) ∧ p(b).

25This rule is known as the cut rule.

26A partial proof is just like a proof, the only difference being that a partial proof might contain leaves which are not axioms, or, as we prefer to call it, which are not closed.

To proceed, we have no choice but to apply the beta rule “introduction of ∧ in the succedent”. After the application of this rule, the partial proof constructed thus far takes the following form:

p(t) ⊢ p(a) p(t) ⊢ p(b)
p(t) ⊢ p(a) ∧ p(b)
∀x.p(x) ⊢ p(a) ∧ p(b)

To finish this proof, we have to find a term t which can be substituted for the metavariable t so that the leaves of the partial proof tree above are turned into axioms. Now it is easy to see that substituting a for t turns the left leaf into an axiom while the substitution which substitutes b for t turns the right leaf into an axiom. Unfortunately we are only allowed to make one substitution and therefore we are not able to finish our proof. Now there are two ways out of this dilemma. If we had reversed the order of our rule applications and had started by applying the β rule first we would have ended up with the following proof tree:

\frac{p(t_{1}) ⊢ p(a)}{∀x.p(x) ⊢ p(a)}  \frac{p(t_{2}) ⊢ p(b)}{∀x.p(x) ⊢ p(b)}
∀x.p(x) ⊢ p(a) ∧ p(b)

By substituting a for t_{1} and b for t_{2} this can be turned into a valid proof. This shows that γ rules should only be applied after all possible β rules have been applied. Of course, this is the tactic used by Seduct. However, this tactic is not always sufficient. There are examples where really more than one substitution for a metavariable is needed. To deal with these cases, one needs an analytical version of the γ rules. This version of the γ rules has the following form:

1. Introduction of ∀ in the antecedent:

\frac{Γ, ∀x.P, P [x ← t] ⊢ Δ}{Γ, ∀x.P ⊢ Δ}(∀A)

2. Introduction of ∃ in the succedent:

\frac{Γ ⊢ Δ, ∃x.P, P [x ← t]}{Γ ⊢ Δ, ∃x.P}(∃S)

The problem with this version of the γ rules is that the premise is now more complex than the conclusion. Therefore a direct implementation of these rules could lead to a nonterminating proof search. To solve this problem, Seduct marks the quantified formulas displayed in the premisses of these rules as being used. Seduct will not use them again while in automatic mode. Instead, if a proof search fails, the user has to decide which γ rules may be applied to a marked quantified formula to proceed with the proof.

Fortunately, the γ rules are the only rules whose application can cause the failure of the search for a proof of a valid theorem. This explains that we have to be very careful with the application of γ rules and that we should try to avoid them completely in favour of the other rules. That was our reason for introducing additional α and δ rules. These additional rules are just given to be able to avoid the application of γ rules as long as possible.

5.8 The δ Rules

Classically, the following rules are referred to as δ rules:

1. Introduction of ∀ in the succedent:

\frac{Γ ⊢ Δ, P [x ← c]}{Γ ⊢ Δ, ∀x.P}(∀S)

The application of this rule is subject to the condition that the constant c does not occur in the sequent Γ ⊢ Δ, ∀x.P. This condition is also known as the eigenvariable condition.

2. Introduction of ∃ in the antecedent:

\frac{Γ, P [c/x] ⊢ Δ}{Γ, ∃x.P ⊢ Δ}(∃A)

The application of this rule is also subject to the eigenvariable condition: The constant c must not occur in the sequent Γ, ∃x.P ⊢ Δ.

To these rules we add two more which do not introduce new constants but rather new functions, sometimes referred to as Skolem functions.

1. Introduction of ∀ in the succedent under an existential quantifier:

\frac{Γ ⊢ Δ, ∃x⃗.P [y ← s(x⃗)]}{Γ ⊢ Δ, ∃x⃗.∀y.P}(∃∀S)

provided that the Skolem function s does not occur in the sequent Γ ⊢ Δ, ∃x⃗.∀y.P.

2. Introduction of ∃ in the antecedent under an universal quantifier:

\frac{Γ, ∀x⃗.P [y ← s(x⃗)] ⊢ Δ}{Γ, ∀x⃗.∃y.P ⊢ Δ}(∀∃A)

provided that the Skolem function s does not occur in the sequent Γ, ∀x⃗.∃y.P ⊢ Δ.

5.9 Additional Rules for Dealing with Quantifiers

Sometimes a quantifier quantifies a variable which occurs only in a part of the quantified formula. In this case it may be beneficial to distribute this quantifier over its subformulas, if thereby the application of a γ rule can be avoided. Therefore we add the following rules to our calculus:

1. There are two rules dealing with the distribution of a ∀ quantifier over a disjunction in the antecedent:

\frac{Γ, ∀y⃗(A ∨ ∀x B) ⊢ Δ}{Γ, ∀x∀y⃗ (A ∨ B) ⊢ Δ}  \frac{Γ, ∀y⃗(∀x A ∨ B) ⊢ Δ}{Γ, ∀x∀y⃗ (A ∨ B) ⊢ Δ}
provided x does not occur in A.  provided x does not occur in B.

2. There are two rules dealing with the distribution of a ∀ quantifier over an implication in the antecedent:

\frac{Γ, ∀y⃗(A → ∀x B) ⊢ Δ}{Γ, ∀x∀y⃗ (A → B) ⊢ Δ}  \frac{Γ, ∀y⃗(∃x A → B) ⊢ Δ}{Γ, ∀x∀y⃗ (A → B) ⊢ Δ}
provided x does not occur in A.  provided x does not occur in B.

3. There are two rules dealing with the distribution of an ∃ quantifier over a conjunction in the succedent:

\frac{Γ ⊢ Δ, ∃y⃗(∃x A ∧ B)}{Γ ⊢ Δ, ∃x ∃y⃗(A ∧ B)}  \frac{Γ ⊢ Δ, ∃y⃗(A ∧ ∃x B)}{Γ ⊢ Δ, ∃x ∃y⃗(A ∧ B)}
provided x does not occur in B.  provided x does not occur in A.

These rules give us no possibility to distribute a quantifier over an equivalence. The following rules are designed to achieve this purpose:

\frac{Γ, A, ∀x B ⊢ Δ  Γ ⊢ Δ, A, ∃x B}{Γ, ∀x(A ↔ B) ⊢ Δ}  \frac{Γ, A ⊢ Δ, ∀x B  Γ, ∃x B ⊢ Δ, A}{Γ ⊢ Δ, ∀x(A ↔ B)}

\frac{Γ, A, ∃x B ⊢ Δ  Γ ⊢ Δ, A, ∀x B}{Γ, ∃x(A ↔ B) ⊢ Δ}  \frac{Γ, ∀x B ⊢ Δ, A  Γ, A ⊢ Δ, ∃x B}{Γ ⊢ Δ, ∃x(A ↔ B)}

The provision to apply any of these rules is that the variable x must not occur in A. Of course, there are analogous rules for the case that x does not occur in B. For reasons of space, they are not given here.

5.10 The ι Rules

Since Seduct is constructed to be used in the context of program verification, it is not only capable of dealing efficiently with full first–order logic with equality, but also with inequalities. By this we mean that certain features of the inequality symbols “≤”, “<”, “≥” and “>” have been implemented in Seduct. This is achieved via the following set of rules which we have termed ι rules:

1. Introduction of < in the antecedent:

\frac{Γ, s ≤ t ⊢ Δ, s = t}{Γ, s < t ⊢ Δ}

2. Introduction of > in the antecedent:

\frac{Γ, s ≥ t ⊢ Δ, s = t}{Γ, s > t ⊢ Δ}

3. Introduction of ≤ in the succedent:

\frac{Γ, s ≥ t ⊢ Δ, s = t}{Γ ⊢ Δ, s ≤ t}

4. Introduction of ≥ in the succedent:

\frac{Γ, s ≤ t ⊢ Δ, s = t}{Γ ⊢ Δ, s ≥ t}

5. Introduction of < in the succedent:

\frac{Γ, s ≥ t ⊢ Δ}{Γ ⊢ Δ, s < t}

6. Introduction of > in the succedent:

\frac{Γ, s ≤ t ⊢ Δ}{Γ ⊢ Δ, s > t}

Which axioms concerning the symbols ≤, ≥, < and > do these rules reflect? First of all, ≤ is intended to denote a total ordering, that is to say ≤ satisfies the following axioms:

1. x ≤ x (Reflexivity)

2. x ≤ y ∧ y ≤ x → x = y (Antisymmetry)

3. x ≤ y ∧ y ≤ z → x ≤ z (Transitivity)

4. x ≤ y ∨ y ≤ x (Linearity)

Furthermore, the following axioms establish a relation between ≤ on the one hand and ≥, < and > on the other hand:

• Relation between ≤ and ≥: x ≤ y ↔ y ≥ x.
• Relation between ≤ and <: x < y ↔ x ≤ y ∧ x ≠ y.^{27}
• Relation between ≥ and >: x > y ↔ x ≥ y ∧ x ≠ y.
• Relation between < and >: x < y ↔ y > x.

If we take a closer look at the ι rules given above, we recognize that there backward application eliminates the symbols < and > from the antecedent and succedent, while ≤ and ≥ are only eliminated from the succcedent. To eliminate ≤ and ≥ from the antecedent, we need two additional rules:

27The notation x ≠ y is just a convenient shorthand for the formula ¬(x = y).

1. Introduction of ≤ in the antecedent:

\frac{Γ, s = min(s, t) ⊢ Δ}{Γ, s ≤ t ⊢ Δ}.

2. Introduction of ≥ in the antecedent:

\frac{Γ, t = min(s, t) ⊢ Δ}{Γ, s ≥ t ⊢ Δ}.

These rules takes care of the axioms of reflexivity, antisymmetry and transitivity because these properties are reflected by the idempotence, symmetry and associativity of the min operator.

In addition to the ι–rules given so far we have implemented six more rules which are useful since they can be used to avoid γ–rules. These rules take the following form:

1. Introduction of < under ∃ in the succedent:

\frac{Γ, ∀x⃗.t ≤ s ⊢ Δ}{Γ ⊢ Δ, ∃x⃗.s > t}

2. Introduction of > under ∃ in the succedent:

\frac{Γ, ∀x⃗.t ≥ s ⊢ Δ}{Γ ⊢ Δ, ∃x⃗.s < t}

3. Introduction of ≤ under ∃ in the succedent:

\frac{Γ, ∀x⃗.t ≤ s ⊢ Δ, ∃x⃗.s = t}{Γ ⊢ Δ, ∃x⃗.s ≤ t}

4. Introduction of ≥ under ∃ in the succedent:

\frac{Γ, ∀x⃗.t ≥ s ⊢ Δ, ∃x⃗.s = t}{Γ ⊢ Δ, ∃x⃗.s ≥ t}

5. Introduction of < under ∀ in the antecedent:

\frac{Γ, ∀x⃗.s ≤ t ⊢ Δ, ∃x⃗.s = t}{Γ, ∀x⃗.s < t ⊢ Δ}

6. Introduction of > under ∀ in the antecedent:

\frac{Γ, ∀x⃗.s ≥ t ⊢ Δ, ∃x⃗.s = t}{Γ, ∀x⃗.s > t ⊢ Δ}

5.11 An Example

We will now give a simple example illustrating the way Seduct searches for a proof. Suppose Seduct is to prove the formula

∀x.(p(x) → q(x)) → ∀y.p(y) → ∀z.q(z).

Seduct constructs a proof tree with the root

[] ⊢ [∀x.(p(x) → q(x)) → ∀y.p(y) → ∀z.q(z)].

For a start, there is no other possibility than to apply the α rule (→ S) twice.^{28} The partial proof constructed thus far has the form

\frac{\frac{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [∀z.q(z)]}{[∀x.(p(x) → q(x))] ⊢ [∀y.p(y) → ∀z.q(z)]}(→S)}{[] ⊢ [∀x.(p(x) → q(x)) → ∀y.p(y) → ∀z.q(z)]}(→S).

28In principle, after the first application the γ rule (∀A) could also be applied. But SEDUCT never applies a γ rule as long as there is any other rule appliciable.

To reduce the only leaf in this partial proof Seduct uses the δ–rule (∀S). This results in the partial proof

\frac{\frac{\frac{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [q(c)]}{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [∀z.q(z)]}(∀S)}{[∀x.(p(x) → q(x))] ⊢ [∀y.p(y) → ∀z.q(z)]}(→S)}{[] ⊢ [∀x.(p(x) → q(x)) → ∀y.p(y) → ∀z.q(z)]}(→S).

At this stage Seduct has to apply the γ–Regel (∀A). This introduces the metavariable t into the proof tree, which now takes the following form:

\frac{\frac{\frac{\frac{[p(t) → q(t), ∀y.p(y)] ⊢ [q(c)]}{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [q(c)]}(∀A)}{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [∀z.q(z)]}(∀S)}{[∀x.(p(x) → q(x))] ⊢ [∀y.p(y) → ∀z.q(z)]}(→S)}{[] ⊢ [∀x.(p(x) → q(x)) → ∀y.p(y) → ∀z.q(z)]}(→S).

Now the β rule (→A) can be applied to the remaining leaf, giving:

\frac{[q(t), ∀y.p(y)] ⊢ [q(c)] [∀y.p(y)] ⊢ [q(c), p(t)]}{\frac{\frac{\frac{\frac{[p(t) → q(t), ∀y.p(y)] ⊢ [q(c)]}{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [q(c)]}(∀A)}{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [∀z.q(z)]}(∀S)}{[∀x.(p(x) → q(x))] ⊢ [∀y.p(y) → ∀z.q(z)]}(→S)}{[] ⊢ [∀x.(p(x) → q(x)) → ∀y.p(y) → ∀z.q(z)]}(→S).}(→A)

At this point Seduct realizes that by substituting the Skolem constant c for the metavariable t the leave in the left branch of this proof tree can be turned into an axiom. The leaf in the right branch is then recognized as an axiom too since the formula p(c) in the succedent is an instance of the formula ∀y.p(y) in the antecedent. Altogether, the complete proof looks like the following:

\frac{[q(c), ∀y.p(y)] ⊢ [q(c)] [∀y.p(y)] ⊢ [q(c), p(c)]}{\frac{\frac{\frac{\frac{[p(c) → q(c), ∀y.p(y)] ⊢ [q(c)]}{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [q(c)]}(∀A)}{[∀x.(p(x) → q(x)), ∀y.p(y)] ⊢ [∀z.q(z)]}(∀S)}{[∀x.(p(x) → q(x))] ⊢ [∀y.p(y) → ∀z.q(z)]}(→S)}{[] ⊢ [∀x.(p(x) → q(x)) → ∀y.p(y) → ∀z.q(z)]}(→S).}(→A)

6 The Rewriting Techniques Employed by SEDUCT

Reasoning about equations is a substantial part of theorem proving. Often one has to prove that a given equation follows from an algebraic^{29} theory. The most effective procedure for solving problems of this kind is the rewriting procedure. For now we will give a rough, rather informal overview of rewriting. Later subsections will give a more formal and complete description.

The central idea of rewriting is simplification. The aim of simplification is to replace a complex term by a less complex term which is equal to the original complex term in the theory under investigation. To be able to apply the rewriting technology when working in an algebraic theory, the equations axiomatizing this theory have to be oriented in such a way that they can be used to simplify expressions. These oriented equations are called rewrite rules. To make things more concrete, consider the following example describing the concatenation of lists. The function concat is defined by:

\begin{aligned}concat( nil, x ) & = & x \\ concat( cons(x, y), z ) & = & cons( x, concat(y, z) ) \end{aligned}

These axioms are oriented from left to right. They can be used to simplify the term

concat(cons(a, cons(b, nil)), nil)

via the following chain of equations:

concat(cons(a, cons(b, nil)), nil) = cons(a, concat(cons(b, nil), nil))
= cons(a, cons(b, concat(nil, nil)))
= cons(a, cons(b, nil))

The procedure to prove a given conjecture s = t by rewriting is the following: Simplify both s and t as much as possible using the given axioms. This process of successive simplifications is also known as normalisation. The result of this normalization is called a normal form. If the normal forms of s and t are identical, the equation s = t has been proved. However, this process is not always successful. Consider the following set of equations:

1. (x ∗ y) ∗ z = x ∗ (y ∗ z) (Associativity)
2. e ∗ x = x  (Left Neutral)
3. i(x) ∗ x = e  (Left Inverse)

These axioms are a complete axiomization for group theory, where e denotes the neutral element and i(x) is the inverse of x. Therefore every equation valid in group theory can be deduced from these three equations. For instance, the equation

i(x) ∗ (x ∗ y) = y  (1)

is provable in group theory. However, this equation is not provable by rewriting if we use only the three axioms given above oriented from left to right. This is easy to see since both the term i(x) ∗ (x ∗ y) and the term y are in normal form with respect those three equations. So how can we possibly prove (1) by rewriting? The answer is simple: We have to complete the original rewrite system by adding some derived axioms. The aim of this completion is to get a rewrite system which has the Church–Rosser property. A rewrite system has the Church–Rosser property if for any term s that can be simplified to either t_{1} or t_{2}, there is a term t such that both t_{1} and t_{2} can be further simplified to yield t. In symbols, this can be written as:

(s →^{∗} t_{1} ∧ s →^{∗} t_{2}) ⇒ ∃t.(t_{1} →^{∗} t ∧ t_{2} →^{∗} t)

(The notation l → r is used to express the fact that l can be simplified to r using one equation. We write l →^{∗} r to express the fact that l can be simplified by successive application of 0 or more equations.)

29We call a theory algebraic if all of its axioms are equations.

Starting from a set of equations, how do we construct a rewrite system which has the Church–Rosser property? The answer to this question was given by Knuth and Bendix [9] by introducing the notion of critical pairs. For now, we will only give an informal account of this notion. Consider the rules

(x ∗ y) ∗ z → x ∗ (y ∗ z) and i(u) ∗ u → e.

If we take the first rule and substitute i(u) for x and u for y we will get the new rule (i(u) ∗ u) ∗ z → i(u) ∗ (u ∗ z). But the left hand side (i(u) ∗ u) ∗ z of this new rule can by construction also be simplified via the second rule i(u) ∗ u → e to yield the term e ∗ z. So the left hand side can be simplified in two ways:

(i(u) ∗ u) ∗ z → i(u) ∗ (u ∗ z) and (i(u) ∗ u) ∗ z → e ∗ z.

The two terms to which (i(u) ∗ u) ∗ z can be reduced build a critical pair. Since the two terms of this critical pair can not be reduced to a common normal form by the old rules, we have deduced a useful new equation. Now the seminal idea is to take this equation, orient it into a rewrite rule and add it to the original rules. In our case we would add the rule

i(u) ∗ (u ∗ z) → e ∗ z.

This process proceeds as long as it produces new rules. If this process stops because all remaining critical pairs can be simplified to a triviality with the help of the given rules, the resulting term rewriting system is guaranteed to possess the Church–Rosser property. If we start this process for the axioms of group theory, we get the following system of rewrite rules:

\begin{matrix}1. & e ∗ x → x & 2. & i(x) ∗ x → e \\ 3. & (x ∗ y) ∗ z → x ∗ (y ∗ z) & 4. & i(x) ∗ (x ∗ y) → y \\ 5. & x ∗ e → x & 6. & i(e) → e \\ 7. & i (i(x)) → x & 8. & x ∗ i(x) → e \\ 9. & x ∗ (i(x) ∗ y) → y & 10. & i(x ∗ y) → i(y) ∗ i(x) \end{matrix}

This system has got the Church–Rosser property. Therefore it is capable of deciding any equation in group theory. If s = t is the conjecture the truth of which is to be investigated, we just have to normalize s and t using the system just given. If the normal forms are identical, s = t is true in group theory, otherwise it is false.

The process to complete a rewrite system can fail for two reasons. For one thing, the process is not guaranteed to stop. In this case there is no remedy. This case reflects the fact that first–order logic is undecidable, even if we restrict ourselves to equations. The other possible reason for failure is the production of a critical pair which can not be oriented into a rewrite rule. For instance, asssume that our procedure yields a critical pair of the form (x ∗ y, y ∗ x). Apparently the corresponding equation x ∗ y = y ∗ x can not be directed sensibly. However, by extending the notion of rewriting a little bit we can solve this problem. The new notion is termed ordered rewriting. The basic idea behind ordered rewriting is that although an equation like x ∗ y = y ∗ x can not be oriented, it might have orientable instances. These instances could then be used for simplification. For example, assume a and b are constants and take a look at the term b ∗ a. Assume further that there is an ordering on the set of terms under which a ∗ b is smaller than b ∗ a. Then b ∗ a could be rewritten to a ∗ b using the equation x ∗ y = y ∗ x.

Up to now we have been quite informal. In the following subsections this will change. We think that it will be safe for most of our users to skip these subsections. However, to get a thorough understanding of how Seduct finds proofs, they are essential.

6.1 Basic Definitions

In this and the following subsection we will elaborate on the informal explanation of rewriting which we have given above. For reasons of space and time we will not be able to give a fully self contained exposition of term rewriting technology. In particular we will not prove any theorems guaranteeing that our method of proof search is complete. For these more theoretical issues the reader is advised to consult either the article by Dershowitz & Jouannaud [3] or the excellent book by Leo Bachmair [1].

We start with some definitions. To prevent things from getting too involved we will restrict our attention to the single–sorted case. The set of all terms is denoted by T (F, V), where F denotes the set of all function symbols used to build terms, while V is the set of all variables. The set of all ground terms, i.e. the set of all terms containing no variables, is written as T (F). The set of all variables occurring in a term t is written as F V (t). A substitution is a mapping from the set V of all variables to the set T (F, V) of all terms. Substitutions are lifted to terms in the usual way. The set of all substitutions is denoted by Σ. We use lowercase Greek letters like σ, μ and ϱ to denote substitutions. If σ is a substitution and t is a term we write tσ instead of σ(t). The term tσ is called an instance of t. If s and t are terms and σ is a substitution such that sσ ≡ tσ, then σ is called a unifier of s and t. The most general unifier of s and t is written as mgu(s, t). We write s ≡ t if we want to express that s and t denote the same term. If we just want to state that s and t are equal in some theory this is written as s = t.

Next we define the set of positions (or occurrences) in a term. These positions can be understood as pointers which give us the possibility to access the subterms of a term. These pointers are realized as lists of natural numbers. Using Prolog notation the empty list is written as [ ] while we write u = [n|v] if u is a list with n as its first element and v as its tail.

The set of positions O(t) of a term t can now be defined by structural induction on terms. Simultaneously we define the expression s/u for a term s and a position u ∈ O(s). Informally, s/u is the subterm of s at position u.

Definition 2 (O(s) und s/u)

1. If s ≡ x ∈ V we define O(s) := {[ ]} and s/[ ] := s.
2. If s ≡ f(s_{1}, ⋯, s_{n}) we define
O(s) = {[ ]} ∪ { [i|u] : 1 ≤ i ≤ n, u ∈ O(s_{i}) } , s/[ ] := s and s/[i|u] := s_{i}/u.

If s and t are terms and u ∈ O(t) is a position in t, then t[u ← s] denotes the term constructed by replacing the subterm at position u in t by s. Formally this could again be defined by structural induction on t.

A non–variable position in a term t is a position u ∈ O(t), such that t/u is not a variable. The set of all

non–variable positions in t is written as O^{∘} (t). Formally, O^{∘} (t) is defined in the following way:

O^{∘} (t) := {u ∈ O(t) : t/u ∉ V}

To ensure that there are no infinite sequences of rewrite operations we have to use well–founded orderings. An ordering on a set X is any binary relation < ⊆ X × X which is irreflexive and transitive. Therefore an ordering < satisfies the following two axioms:

1. x ≮ x for all x ∈ X. (Irreflexivity)

2. x < y ∧ y < z ⇒ x < z for all x, y, z ∈ X. (Transitivity)

An ordering < is well–founded if there does not exist an infinite sequence {x_{n}}_{n∈IN} such that we have

x_{n+1} < x_{n} for all n ∈ IN.

For term rewriting systems we need orderings with certain special properties. These orderings are known as simplification orderings and are defined next.

Definition 3 (Simplification Ordering) An ordering ≺ ⊆ T × T is a simplification–ordering iff for all terms s, t ∈ T (F, V), all function symbols f and all substitutions σ we have the following:

1. s ≺ t ⇒ f(⋯, s, ⋯) ≺ f(⋯, t, ⋯) (Monotonicity)

2. s ≺ f(⋯, s, ⋯). (Subterm Property)

3. s ≺ t → sσ ≺ tσ. (Stability)

It is well–known [3] that every simplification ordering is well–founded. The simplification ordering used by Seduct is the lexicographic path ordering [8, 1, 3]. It is defined next.

Definition 4 (Lexicographic Path Ordering) If < is a linear ordering on the set F of function symbols, then the corresponding lexicographic path ordering <_{lex} on the set of ground terms T (F) is defined by structural induction as follows:

If s ≡ f(s_{1}, ⋯, s_{m}) and t ≡ g(t_{1}, ⋯, t_{n}), then s <_{lex} t if and only if one of the following three cases holds:

0. s is a proper subterm of t.

1. f < g and for all i ∈ {1, ⋯, m} the inequation s_{i} <_{lex} t holds.

2. f = g and there exists an i ∈ {1, ⋯, m} such that the following three conditions hold:

(a) s_{i} <_{lex} t_{i}.

(b) s_{j} ≡ t_{j} for all j ∈ {1, ⋯, i − 1}.
(c) s_{i} <_{lex} t for all j ∈ {i + 1, ⋯, m}.

3. g < f and there is an i ∈ {1, ⋯, n} such that s ≤_{lex} t_{i} holds.^{30}

This ordering is extended to the set T (F, V) of all terms by additionally postulating that for a variable x ∈ V and a term s we have x <_{lex} s if and only if x is a proper subterm of s.

It can easily be verified that the lexicographic path ordering <_{lex} is total on the set of ground terms.

Now we are in a position to define the notion of an ordered term rewriting system. For us, an ordered term rewriting system (TRS for short) is a pair (E, <), where E is a set of equations in T (F, V) and < is a simplification ordering. Usually the equations l = r from E will be written as l → r and will be called rules. If we are talking about a term rewriting system E the simplification ordering < is implicitly understood. A TRS E gives rise to the so called simplification relation →_{E} on T (F, V). This notion is defined next.

Definition 5 (Simplification Relation) A TRS (E, <) induces a binary relation →_{E} on T (F, V), which is defined as s →_{E} t iff the following holds: There exists a position u ∈ O(t), a rule l → r ∈ E and a substitution σ such that

1. s/u ≡ lσ,
2. t ≡ s[u ← rσ], and
3. rσ < lσ.

Informally, this definition states that the term s, which is to be simplified through the TRS (E, <), contains an instance lσ of the left hand side of a rule l → r from E. This instance is then replaced by the corresponding instance rσ of the right hand side of this rule to yield the term t. To ensure that t is smaller with respect to the ordering < we have got the additional condition demanding that rσ < lσ. The monotonicity of the simplification ordering < then guarantees s[u ← rσ] < s[u ← lσ] which is the same as t < s because of condition 2 and because condition 1 implies s ≡ s[u ← lσ]. The notion →_{E} is extended to the notion →_{E}^{∗} which is defined as the transitive and reflexive closure of →_{E}.

A term s is in normal form with respect to a TRS E iff s is not reducible by a rule from E. We call t a normal form of s iff t is in normal form and furthermore s →_{E}^{∗} t holds. Normal forms are unique for a TRS E iff every term has exactly one normal form. It is highly desirable to have a TRS producing unique normal forms because in this case the equational theory given by the equations of the TRS is decidable by a straightforward algorithm: To establish s = t simply compute the normal forms s_{0} and t_{0} of s and t respectivly. If s_{0} ≡ t_{0} the equation s = t holds, otherwise it has been refuted.

There is a straightforward procedure to test whether the normal forms of a TRS E are unique. We just have to check whether critical pairs have a common normal form. This notion is defined next.

30The notation s ≤_{lex} t is a shorthand for the formula s ≡ t ∨ s <_{lex} t.

Definition 6 (Critical Pairs) Suppose there are two rules l → r and s → t in a TRS (E, <) such that the following holds:

1. u ∈O^{∘} (s) is a position pointing to the nonvariable subterm s/u in s.

2. This subterm s/u is unifiable with the left hand side of the rule l → r and the corresponding most general unifier is μ = mgu(s/u, l).

3. We have neither sμ <_{lex} tμ nor lμ <_{lex} rμ.

Then we call (s[u ← r]μ, tμ) a critical pair.

The motivation behind this definition is that if we inspect the term sμ we notice that there may be instances sμσ of it which can be simplified in (at least) two different ways:

sμσ →_{E} tμσ and sμσ →_{E} s[u ← r]μσ.

(We have to take an instance sμσ of the term sμ rather than the term sμ itself because we do not know whether the inequations tμ <_{lex} sμ and rμ <_{lex} lμ hold. The substitution σ has to be chosen in a way such that tμσ <_{lex} sμσ and rμσ <_{lex} lμσ hold. The condition that neither sμ <_{lex} tμ nor lμ <_{lex} rμ holds is added to the definition to eliminate those cases for which we can be sure that there is no such substitution σ.)

6.2 The Rewrite Calculus

The sequent calculus described in the Section 4 is used to reduce the logical structure of the sequents. It reduces the original sequent located at the root of the proof tree to sequents of a certain normal form at the leaves of the tree. If Γ ⊢ Δ is a sequent appearing at a leaf of the proof tree, then we know the following:

• The antecedent Γ consists solely of universally quantified atomic formulas.

• The succedent Δ consists solely of existentially quantified atomic formulas.

The sequent calculus from the Section 4 can recognize these sequents as axioms only in the very special case that

• the antecedent contains a universally quantified formula ∀x⃗.P,

• the succedent contains an existentially quantified formula ∃y⃗.Q, and

• P and Q are (after the possible instantiation of some metavariables) unifiable.

This technique of recognizing axioms completely neglects the properties of the equation symbol. Therefore we need much stronger means to establish sequents of the aforementioned kind as valid. The stronger means we will use are

• rewriting,

• completion, i.e., the construction of critical pairs, and

• narrowing which is a variant of completion.

However, these stronger means only work when applied to equations. Therefore we first have to transform all of our atomic formulas of the form p(t_{1}, ⋯, t_{n}) which are not equations into equations. This is achieved via the following transformation:

p(t_{1}, ⋯, t_{n}) ⇝ p(t_{1}, ⋯, t_{n}) = true iff “p” is different from “=”

The rewrite calculus we are now going to construct differs in a number of ways from the sequent calculus developed in the previous section. First of all, we know that the formulas in the antecedent are universally quantified while the formulas in the succedent are existentially quantified. This fact enables us to simplify the notation by dropping these quantifiers. Secondly, it is no longer necessary to interpret the antecedent and the succedent as multisets. Interpreting them as sets will be sufficient. Therefore a sequent which in the sequent calculus of the Section 4 has the form

[∀x⃗_{1}.P_{1}, ⋯, ∀x⃗_{m}.P_{m}] ⊢ [∃x⃗_{1}.Q_{1}, ⋯, ∃x⃗_{n}.Q_{n}]

will now take the form

{P_{1}, ⋯, P_{m}} ⊢ {Q_{1}, ⋯, Q_{n}}.

This is considerably more concise. To have a handy way of distinguishing between the implicitly universally quantified equations P_{i} in the antecedent and the implicitly existentially quantified equations Q_{j} in the succedent we will refer to the former as rewrite rules while the latter will just be called equations. To make this distinction visible we use the following notation: If s = t is an equation in the antecedent, it will be written as s → t or t → s, where the orientation^{31} depends on the way in which we want to use this equation for rewriting. Since the equations in the succedent are implicitly existentially quantified and can therefore be interpreted as equations to be solved, hereafter we will write an equation s = t from the succedent as s =^{!} t. The reasons for choosing this terminology should soon become clear.

The most important difference between the rules in the rewrite calculus and the rules in the sequent calculus of the previous section is as follows: In the rewrite calculus, all rules are analytical, i.e. the premise is valid if and only if the conclusion is valid. Methodologically, this has an important consequence. To prove a theorem we can now apply rules until we have deduced an axiom, i.e. we are no longer working purely backwards. To give an example, suppose we want to establish the validity of the sequent Γ_{1} ⊢ Δ_{1}. In order to achieve this, we will try to deduce a sequent Γ_{2} ⊢ Δ_{2} from the original sequent. From the second sequent we will try to deduce a third sequent Γ_{3} ⊢ Δ_{3} and so on until we finally will arrive at a sequent Γ_{n} ⊢ Δ_{n} which can be recognized as an axiom. Since for all i ∈ {1, ⋯, n − 1} the validity of the sequent Γ_{i} ⊢ Δ_{i} is equivalent to the validity of Γ_{i+1} ⊢ Δ_{i+1} we are then able to conclude that the sequent Γ_{1} ⊢ Δ_{1} is valid. The whole proof constructed above will be written as:

Γ_{1} ⊢ Δ_{1}

Γ_{2} ⊢ Δ_{2}

\frac{Γ_{3} ⊢ Δ_{3}}{\frac{⋮}{\underline{\underline{Γ_{n} ⊢ Δ_{n}}}}}

The last sequent has been underlined to emphasize that it is an axiom. Notice that this proof is linear, i.e. there is no branching in its proof tree. This is no accident, there are no rules in the rewrite calculus which have two premisses. If there were such rules, working forward would no longer be easy, since then it would be difficult to decide when to apply a rule with two premisses.

We are now in a position to define the rewrite calculus. This calculus is divided into three parts: The axioms, the rules changing the antecedent and the rules changing the succedent. We start with the axioms.

6.3 The Axioms of the Rewrite Calculus

A sequent is an axiom if the succedent contains an equation s =^{!} t whose left hand side s is (after the possible instantiation of metavariables) unifiable with its right hand side t. Formally, we have

\overline{Γ ⊢ Δ ∪ \{s =^{!} t\}}  if s and t are unifiable.

31Occasionally we may have to orient an equation s = t in both ways. This is the case if there are instances of it, where the right hand side is more complex than the left hand side, while for certain other instances it is the other way round. In this case we include s → t as well as t → s as rules into the antecedent.

This axiom is justified by the fact that the equations in the antecedent are implicitly existentially quantified. Furthermore, the succedent is to be interpreted as the disjunction of its constituent equations. Therefore we just need to search the succedent for an equation s =^{!} t such that there is an instantiation of the variables occurring in this equation which identifies s and t.

6.4 Rules Changing the Antecedent

There are five rules changing the antecedent: The first rule is called the superposition rule. Its effect is to add a critical pair to the antecedent. It takes the form:

Γ ∪ {l → r} ∪ {s → t} ⊢ Δ
Γ ∪ {l → r} ∪ {s → t} ∪ {s[u ← r]μ → tμ} ∪ {tμ → s[u ← r]μ} ⊢ Δ

It is subject to the condition that u is a position from O^{∘} (s), such that

μ = mgu(s/u, l), tμ ⪰̸ sμ and rμ ⪰̸ lμ.

This is the most important rule of our calculus because it is the only rule which deduces new information. Next there are two simplification rules. The first simplifies the right hand side of a rule. It is:

\frac{Γ ⊎ \{l → r_{1}\} ⊢ Δ}{Γ ∪ \{l → r_{2}\} ⊢ Δ} provided that r_{1} →_{Γ⊎\{l→r_{1}\}} r_{2} holds.

Here we use the notation A ⊎ B to express the fact that the sets A and B are to be disjoint. The reason for demanding disjointness of Γ and {l → r_{1}} is that we want to be sure that the old rule l → r_{1} is not a member of the antecedent of the new sequent Γ ∪ {l → r_{2}} ⊢ Δ. After all, we want the old rule to be replaced by its simplified version. This can only be guaranteed if the sets {l → r_{1}} and Γ are disjoint.

The next rule simplifies the left hand side of a rule:

\frac{Γ ⊎ \{l_{1} → r\} ⊢ Δ}{Γ ∪ \{l_{2} → r\} ⊢ Δ} provided that l_{1} →_{Γ} l_{2} holds.

Notice the difference with these two simplification rules. While we are allowed to use the rule l → r to simplify its own right hand side r, we are not permitted to do so while simplifying its left hand side l. Otherwise every rule could be simplified into a triviality. This is expressed by allowing Γ ⊎ {l → r_{1}} as index of the rewrite arrow → in the first simplification rule, while we may only use Γ with the second simplification rule.

The splitting rule is used to discover useful constants and functions to be introduced. To motivate this rule, let us consider the equation

(∗)  f(x, y) = g(y, z).

Since the right hand side of this equation does not depend on the variable x, neither does the left hand side. On the other hand, the left hand side does not contain the variable z. This implies that the right hand side can not depend on z either. Altogether we may conclude that both sides depend only on the variable y. We therefore introduce a new function symbol sc and ‘split’ the equation (∗) into two new rules:

f(x, y) → sc(y) and g(y, z) → sc(y)

The example just given motivates the definition of the following rule:

\frac{Γ ⊎ \{l → r\} ⊢ Δ}{Γ ∪ \{l → sc(x_{1}, ⋯, x_{n})\} ∪ \{r → sc(x_{1}, ⋯, x_{n})\} ⊢ Δ} where \{x_{1}, ..., x_{n}\} = F V (l) ∩ F V (r)

(Remember, F V (t) has been defined as the set of all variables occurring in the term t.) Furthermore, this rule is subject to the condition that

F V (r) − F V (l) ≠ ∅ and F V (l) − F V (r) ≠ ∅

hold. The first conditition simply states that there are variables in r not present in l, while the second condition expresses that l possesses variables not present in r. The constant sc used in the rule has to be a new function symbol, i.e. a function symbol not appearing anywhere else, furthermore, it must be of the appropriate arity. It will be referred to as a splitting constant. The splitting rule is added only for efficiency reasons, the calculus would be complete without it.

The last rule is used to eliminate those rules from the antecedent which are no longer applicable because their left hand side has been simplified:

\frac{Γ ⊎ \{l → r\} ⊢ Δ}{Γ ⊢ Δ} provided that r ⪰ l holds.

It is justified by the stability of the ordering ≺. If we have r ⪰ l, then due to the stability of ≺ we already know that rσ ⪰ lσ will hold for every substitution σ. But this implies that the rule l → r will never be applicable because in order to be applicable, we would have to find an instance lσ → rσ of this rule such that rσ ≺ lσ holds. But this last inequality is precluded since we already know that rσ ⪰ lσ must hold.

The rules just given are not applied haphazardly. Rather, they are applied in the following fashion. After building a critical pair (s, t) with the help of the superposition rule, s and t are simplified as much as possible with the existing rules. If s and t reduce to a common normal form, then the critical pair is discarded. If not, we check whether we can split the equation s = t. This is the case if there is a variable occuring on the right hand side only and another variable occuring on the left hand side only. If the splitting rule can not be applied, it is checked whether s ≺ t or t ≺ s holds. In the former case, only the new rule t → s is added, in the latter case, only s → t is added as a new rule. If neither s ≺ t nor t ≺ s is valid both s → t and t → s are added to the antecedent.

After the new rules have been added, all the old rules are simplified as much as possible via the simplification rules. If the left hand side of a rule s_{1} → t has been simplified to s_{2} it is checked whether s_{2} ⪯ t holds. In this case the simplified rule is discarded since it can never be applied.

To summarize, the antecedent is changed in the following way:

1. Select two rules l → r and s → t from the antecedent and build all critical pairs between them.

2. Simplify the resulting critical pairs as much as possible using the equations from the antecedent.

3. Orient the critical pairs which have not been reduced to trivialities into rewrite rules.

4. Simplify the old rewrite rules as much as possible using the newly derived rules.

5. Remove those old rules that are no longer applicable after the simplification because their left hand side has become smaller with respect to the ordering ≺ than their right hand side.

6.5 Rules Changing the Succedent

There are four rules to change the succedent. Firstly, there are two simplification rules:

\frac{Γ ⊢ Δ ⊎ \{s =^{!} t_{1}\}}{Γ ⊢ Δ ∪ \{s =^{!} t_{2}\}} provided that t_{1} →_{Γ} t_{2} holds.

\frac{Γ ⊢ Δ ⊎ \{s_{1} =^{!} t\}}{Γ ⊢ Δ ∪ \{s_{2} =^{!} t\}} provided that s_{1} →_{Γ} s_{2} holds.

Secondly, there are two narrowing rules. They are closely connected to the superposition rule. The first results from superposing a rule onto the left hand side of an equation in the succedent and reads as follows:

Γ ∪ {l → r} ⊢ Δ ∪ {s =^{!} t}

Γ ∪ {l → r} ⊢ Δ ∪ {s =^{!} t} ∪ {s[u ← r]μ =^{!} tμ}

provided that u is a non–variable position in the term s such that the follwing holds:

μ = mgu(s/u, l) and rμ ⪰̸ lμ.

The second is symmetrical and describes the effect of superposing a rule on the right hand side of an equation in the succedent:

Γ ∪ {l → r} ⊢ Δ ∪ {s =^{!} t}

Γ ∪ {l → r} ⊢ Δ ∪ {s =^{!} t} ∪ {sμ =^{!} t[u ← r]μ}

provided that u is a nonvariable position in the term t such that:

μ = mgu(t/u, l) and rμ ⪰̸ lμ.

Again, these rules are not applied haphazardly. Rather, the simplification rules are only applied in two cases. Firstly, they are immediately applied to new equations added by the narrowing rules. Secondly, if a new rule has been added to the antecedent by the superposition rule, this new rule is used to simplify all the equations in the succedent as much as possible.

6.6 The Control Strategy

Having introduced the rewriting calculus, we have to describe the control strategy, i.e. the way in which the rules are applied. We have already described the way in which the simplification rules are linked to the superposition rule and to the narrowing rules. Therefore we only have to specify when to apply narrowing, superposition and splitting. Basically, we have divided the rules and equations into two classes. The first class contains the checked rules and equations while the second class contains the unchecked rules and equations. Initially, all rules and equations are unchecked. The unchecked rules and equations are ordered with respect to their length^{32}. Then the equation or rule which comes first in this ordering is selected. The first thing we do with a selected element is to check it. Now there are two cases. If the element is a rule, we build all critical pairs with all the other rules checked so far. After that we narrow every checked equation with the help of this rule. If, on the other hand, the element is an equation we just use all the rules checked so far to narrow this equation. This process is repeated a certain fixed number of times. This number is controlled by the so called rewrite counter which can be set by the user of Seduct.

6.7 An Example

We conclude this section with an example. It is taken from group theory. Suppose we want to prove the following:

∀x, y, z.(x ∗ y) ∗ z = x ∗ (y ∗ z) ∧ ∀x.1 ∗ x = x ∧ ∀x.∃y.y ∗ x = 1 → ∀x.∃y.x ∗ y = 1  (1)

(Informally, this can be read as the statement that the axioms of group theory imply that every element x has got a right inverse y.) When the sequent calculus is faced with this formula, it creates a proof tree consisting of one branch. The leaf of this branch is marked with the sequent

[ ∀x, y, z.(x ∗ y) ∗ z = x ∗ (y ∗ z), ∀x.1 ∗ x = x, ∀x.s(x) ∗ x = 1 ] ⊢ [ ∃y.c ∗ y = 1 ].  (2)

Since the proof tree contains but a single leaf the proof task has been reduced to the proof of this leaf. The function symbol s and the constant c appearing in the sequent (2) are Skolem constants introduced by the sequent calculus. After transforming this sequent into the representation suitable for our rewrite calculus it takes the following form:

{ (x ∗ y) ∗ z → x ∗ (y ∗ z), 1 ∗ x → x, s(x) ∗ x → 1 } ⊢ { c ∗ y =^{!} 1 }.  (3)

32Well, there are some other ingredients beside the length of the terms when it comes to ordering them. But for reasons of space and time we can not discuss every detail here.

For reasons of space we will not present the following derivation in minute detail. We will rather concentrate on the significant steps. We start by building critical pairs between the rules

s(x) ∗ x → 1 and (x ∗ y) ∗ z → x ∗ (y ∗ z).

Since the subterm x ∗ y on the left hand side of the second rule is unifiable with the left hand side s(x) ∗ x of the first rule, we find the critical pair (1 ∗ y, s(x) ∗ (x ∗ y)). Using the rule 1 ∗ x → x this can be simplified to (y, s(x) ∗ (x ∗ y)). Since we will have y ≺ s(x) ∗ (x ∗ y) in any simplification ordering ≺, the rule s(x) ∗ (x ∗ y) → y is added to the antecedent. Since none of the other rules and equations can be simplified with this new rule, we arrive at the new sequent

{ (x ∗ y) ∗ z → x ∗ (y ∗ z), 1 ∗ x → x, s(x) ∗ x → 1, s(x) ∗ (x ∗ y) → y } ⊢ { ∃y.c ∗ y =^{!} 1 }.  (4)

We can build a critical pair with the rule just added and the rule s(x)∗x → 1. This critical pair is (s(s(x))∗1, x). Since we have x ≺ s(s(x)) ∗ 1 for any simplification, this is oriented into the new rule

s(s(x)) ∗ 1 → x.  (5)

As critical pair between (5) and the rule (x ∗ y) ∗ z → x ∗ (y ∗ z) we find (x ∗ y, s(s(x)) ∗ (1 ∗ y)) which can be simplified to (x ∗ y, s(s(x)) ∗ y). This is oriented into the equation

s(s(x)) ∗ y → x ∗ y.  (6)

Superposition of (5) and (6) results in the new critical pair (x ∗ 1, x), which is immediatedly turned into the rule

x ∗ 1 → x.  (7)

Now rule (5) can be simplified to

s(s(x)) → x.  (5′)

This simplified rule can be used to build critical pairs with the rule s(x) ∗ x → 1. Doing so we find the critical pair (x ∗ s(x), 1). Turning this into a rule provides us with

x ∗ s(x) → 1.  (8)

This last rule is then used to narrow the equation c ∗ y =^{!} 1 into the equation 1 =^{!} 1 which is obviously an axiom. This finishes our proof. The last step can be interpreted as substituting s(c) for the variable y in the equation c ∗ y =^{!} 1. After this substitution this equation takes the form c ∗ s(c) =^{!} 1 which can in turn be reduced to a triviality via the rule (8).

7 Commands Available in SEDUCT

This section consists of a description of the various modes in which the Seduct command interpreter is operating, a list of notational and other short-hands used in this section, and a list of the commands available in Seduct.

Basically, the Seduct command interpreter reads a command completed by a full stop (“.”), parses it, executes it possibly changing the state of Seduct (including the mode of the command interpreter), and then repeats this process for a new command. The execution of a single Seduct command can be interrupted by pressing Ctrl-C. This causes Seduct to prompt for a new command in the state from before entering the interrupted command. To stop the interactive execution of a proof, the abort command described on page 90 is used.

7.1 Command Interpreter Modes

Seduct operates in various modes which affect the availability and effects of commands. These are:

Prove mode: This mode is entered by executing the prove command. It enables the commands that are only available in this mode. Seduct leaves this mode when the last outstanding proof has been completed (for example by a go command) or abandoned (for example by an abort command). Prove mode is indicated by a prompt of the form SEDUCT(Goal Name). After completion or abortion of a proof which was initiated by a prove command while already in prove mode, Seduct stays in prove mode, of course.

Believe mode: This mode is entered by means of the begin( believe ) command, and exited by means of a corresponding end( believe ) command. In this mode, the prove command does not put Seduct in prove mode, but simply marks the goal as proved. In believe mode, the prove mode commands have no effect. Thus, during the development of a proof, begin/end( believe ) pairs can be used to bracket proofs of lemmas, relieving the user from unnecessary delays when these proofs are repeatedly executed.

Macro definition mode: This mode is entered by the macro command and exited by a corresponding end command. In this mode, commands are not executed, but recorded as part of the macro being defined. Commands are not checked for legality since in the presence of formal parameters this is not possible.

Strict mode: Seduct is by default in this mode. It is exited by executing the unset( strict ) commands, and re-entered by executing the set( strict ) command. In this mode, commands like remove and believe which can compromise the correctness of a proof, are not available.

There is a hierarchy to these modes in the following sense: In macro definition mode, the other modes have no significance, in believe mode, prove mode has no effect. Strict mode is orthogonal to prove and macro definition mode.

7.2 Short-hands

The various short-hands used in this section are:

• if a command requires the current goal to be of the form:

forall( [ x_{1}: sort_{1}, ⋯, x_{n}: sort_{n} ], F )

then the following form is also accepted:

      forall( x: sort, F )

• The stack of sequents is called the goal stack, and the the word goal is used for the succedent of a sequent or even for a sequent. It should always be clear from the context which meaning is intended.

• To improve readability, Seduct commands embedded in normal text are often written without the final full stop (“.”).

• The notation G[ x_{1} ← E_{1}, ⋯, x_{n} ← E_{n}] stands for a formula or term G in which every occurrence of each of the variables x_{1}, ⋯, x_{n} has been replaced by E_{1}, ⋯, E_{n}, respectively.

7.3 Commands Available in SEDUCT in Any Mode

7.3.1 arity

This command takes one parameter. Its syntax is

arity( Declaration ). It is used to add arity declarations to the database. There are three types of arity declarations: constant declarations, function declarations, and predicate declarations. To declare a constant, the following syntax is used:

arity( c: sort ). This will declare the symbol c to be a constant of sort sort. A function declaration has the form:

      arity( f: [ sort_{1}, ..., sort_{n} ] -> sort ).

This declaration declares f as a function with the cartesian product sort_{1} × ⋯ × sort_{n} as domain and the sort sort as range. None of the sorts sort_{1}, ..., sort_{n} is allowed to be bool. If the function symbol f either is an infix operator or has been declared as an infix operator, it is necessary to put f into parentheses. For example, symbols like “+” and “-” would have to be set into parentheses as in

      arity( (+): [ nat, nat ] -> nat ).

Moreover, operators containing a full stop have to be quoted since a non-quoted indicates the end of a command to the parser. For more information, see appendix A.

Finally, a predicate declaration takes the form:

      arity( p: [ sort_{1}, ..., sort_{n} ] -> bool ).

This declaration will declare p as a predicate defined on the cartesian product sort_{1} × ⋯ × sort_{n}. None of the sorts sort_{1}, ..., sort_{n} is allowed to be bool.

The user defined symbols may not be overloaded, for example it is not allowed to define the same symbol h both as a predicate symbol and as a function symbol. If an attempt is made to add a declaration for a symbol which has already been defined, an error message is issued.

7.3.2 associative commutative

This command takes one parameter. Its syntax is

      associative commutative( f ).

The effect of this command is to declare the function f as being associative and commutative. For this to make any sense, f must be a binary function symbol which is declared by a declaration of the form

f: [ sort, sort ] -> sort. Logically, this command is equivalent to asserting the axioms of associativity and commutativity given below:

      forall( [ x: sort, y: sort, z: sort ], f(f(x,y),z) = f(x,f(y,z)) ).  (Associativity)
      forall( [ x: sort, y: sort ], f(x,y) = f(y,x) ).  (Commutativity)

These axioms are implemented by adding three rewrite rules to the database. These rules are the following:

      f(x,y) → f(y,x).
      f(x,f(y,z)) → f(y,f(x,z)).
      f(f(x,y),z) → f(x,f(y,z)).

During completion the effect of these rewrite rules is simulated by a sorting procedure since this is more efficient than ordinary rewriting.

7.3.3 associative commutative idempotent

This command takes one parameter. Its syntax is

      associative commutative idempotent(f).

The effect of this command is to declare the function f as being associative, commutative and idempotent. For this to make any sense, f must be a binary function symbol which is declared by a declaration of the form

f: [ sort, sort ] -> sort. Logically, this command is equivalent to asserting the axioms of associativity, commutativity and idempotence given below:

      forall( [ x: sort, y: sort, z: sort ], f(f(x,y),z) = f(x,f(y,z)) ).  (Associativity)
      forall( [ x: sort, y: sort ], f(x,y) = f(y,x) ).  (Commutativity)

forall( x: sort, f(x,x) = x ). (Idempotence) These axioms are implemented by adding the following rewrite rules to the database:

      f(x,y) → f(y,x).
      f(x,f(y,z)) → f(y,f(x,z)).
      f(f(x,y),z) → f(x,f(y,z)).
      f(x,x) → x.
      f(x,f(x,y)) → f(x,y).

During completion the effect of these rewrite rules is simulated by a sorting procedure since this is more efficient than ordinary rewriting.

7.3.4 axiom

This command takes one parameter and has the form:

      axiom( Name: F ).

Execution of this command asserts the formula F, which has to be a closed formula, as a new axiom which can be referred to by the name Name.

7.3.5 begin( axioms )

This command takes no parameters and is closed by the command end( axioms ). It has the form:

      begin( axioms ).

axiom declarations

      end( axioms ).

Here axiom declarations is a sequence of declarations of axioms. A declaration of an axiom has the form:

Name: Formula.

The execution of this command asserts each formula Formula, which has to be closed, as a new axiom which can be referred to by the name Name.

7.3.6 begin( believe )

This command puts Seduct in believe mode. The effect of this command is negated by an end( believe ) command. Believe blocks can be nested, so to leave believe mode, the same number of end( believe ) commands as begin( believe ) commands must be entered.

In believe mode, prove mode commands have no effect and the goal of a prove command is implicitly believed to be true, i.e. if the following goal has been defined:

name: G then the command

prove( name, Theory ). in believe mode, has approximately the same effect as the two commands

      remove( goal, name ).
      axiom( name: G ).

The difference being that the prove command in believe mode asserts name not as an axiom but as a theorem.

7.3.7 begin( declare )

This command takes no parameters and starts a section with arity declarations. It is closed by the command end( declare ). Its syntax is as follows:

      begin( declare ).

arity declarations

      end( declare ).

Here arity declarations is a sequence of arity declarations. The syntax of an arity declaration has got one of the following three possibilities:

c: sort.

f: [ sort_{1}, ..., sort_{n} ] -> sort.

         p: [ sort_{1}, ..., sort_{n} ] -> bool.

The first possibility declares c to be a constant of sort sort, the second declares f as a function with the cartesian product sort_{1} × ⋯ × sort_{n} as domain and the sort sort as range. If the function symbol f either is an infix operator or has been declared as an infix operator, it is necessary to put f into parentheses. For example, symbols like “+” and “-” would have to be set into parentheses as in

      (+): [ nat, nat ] -> nat.

Moreover, operators containing a full stop have to be quoted since a non-quoted indicates the end of a command to the parser. For more information, see appendix A.

By the third possibility a predicate p is specified on the cartesian product sort_{1} × ⋯ × sort_{n}. For the function declaration as well as the predicate declaration, is neither of the sorts sort_{1}, ..., sort_{n} allowed to be

bool.
7.3.8 begin( definitions )

This command takes no parameters and is closed by end( definitions ). It starts a section of definition declarations and has the following form:

      begin( definitions ).

definition declarations

      end( definitions ).

definition declarations is a sequence of definition declarations. A definition declaration has the following syntax:

Name: F.

Execution of this command asserts each formula F as a new definition which can be referred to by the name Name.

The formula F must have a specific form. There are two possibilities:

First, F can be a formula without any variables of one of the following forms:

C -> T = S or

           C -> ( P <--> Q ).

Here, S and T are closed terms and P is a prime formula without variables while C and Q are closed formulae.

Secondly, F can be a universally closed formula of one of the following forms:

           forall( [ x_{1}: sort_{1}, ..., x_{n}: sort_{n} ], C -> ( P <--> F ) )  or

           forall( [ x_{1}: sort_{1}, ..., x_{n}: sort_{n} ], C -> S = T ).

Here, P is an atomic formula and C and F are closed formulae, and S and T are terms.

In both cases, formulae of the form P and ^P are regarded as abbreviations for P <--> true and P <--> false, respectively. Moreover, unconditional equations of the form S = T or P <--> F are regarded as abbreviations for true -> S = T and true -> P <--> F, respectively.

7.3.9 begin( goals )

This command takes no parameters and starts a section of goal declarations which is closed by end( goals ). It has the following syntax:

      begin( goals ).

Goal Declaration Sequence

      end( goals ).

Goal Declaration Sequence is a sequence of goal declarations. A goal declaration has the following syntax:

Name: F.

The execution of this command asserts the formula F as new goal to be proved later. This goal can be referred to by its name Name.

7.3.10 begin( operators )

This command takes no parameters and starts a section with operator precedence declarations. It is closed by the command end( operators ). It has got the following syntax:

      begin( operators ).

Operator Declaration Sequence

      end( operators ).

Operator Declaration Sequence is a sequence of operator declarations. The syntax of an operator declaration is as follows:

op: n.

where op is the name of a function or constant symbol which must have been declared before and n is a natural number between 0 and 1000. If the function symbol f either is an infix operator or has been declared as an infix operator, it is necessary to put f into parentheses. For example, symbols like “+” and “-” would have to be set into parentheses as in

      (+): 2.

Moreover, operators containing a full stop have to be quoted since a non-quoted indicates the end of a command to the parser. For more information, see appendix A.

7.3.11 begin( theories )

This command takes no parameters. It starts a section with theory declarations which is closed by end(theories). It has the form:

      begin( theories ).

Theory Declaration Sequence

      end( theories ).

Theory Declaration Sequence is a sequence of theory declarations. The syntax of a theory declaration is:

T = D.

Its effect is to define a new theory D named T. The theory definition D is either a list consisting of axiom names, definition names, theorem names and goal names, or it is of the form

D_{1} + D_{2}

where D_{1} and D_{2} are theory definitions. If a theory contains goals it can only be used after these goals have been proved and thereby turned into theorems.

7.3.12 begin( time )

This command starts a time measurement. The measurement is completed by the end( time ) command (cf. section 7.3.19).

7.3.13 clear This command takes no parameters and has the form:

      clear.

The effect of this command is to clear the memory from all declarations, axioms, goals, theorems and the like, except for a few predefined functions and constants. Furthermore, some global variables are reset to their default value. Effectively, this corresponds to executing the following commands:

      do not show proof.
      unset( check ).
      set( strict ).
      unset( auto show ).

The meaning of these commands is explained in the appropriate sections of this chapter. Moreover, all operators are reset to their predefined meanings, i.e. all user defined operators are deleted.

7.3.14 close This command takes no parameters and has the form:

      close.

This command is used to close output files which have been opened by the protocol command. If the current output has not been redirected to a protocol file, the close command has no effect.

7.3.15 definition

This command takes one parameter and has the form:

      definition( Name: F ).

Execution of this command asserts the formula F as a new definition which can be referred to by the name Name.

The formula F has to be a closed one and must have a specific form. There are two different possibilities: First, F can be a formula without any variables of one of the two following forms:

t = s or

      P <--> Q.

Here, s and t are terms not containing any variables and P and Q are prime formulae, also containing no variables.

Secondly, F can be a universally closed formula of one of the two following forms:

      forall( [ x_{1}: sort_{1}, ..., x_{n}: sort_{n} ], P <--> F )  or
      forall( [ x_{1}: sort_{1}, ..., x_{n}: sort_{n} ], s = t ).

Here, P is an atomic formula and F is any other closed formula, and s and t are terms.

In both cases, formulae of the form P and ^P are regarded as abbreviations for p <--> true and P <--> false, respectively.

7.3.16 disjoint

This command takes two parameters and has the form:

      disjoint( f, g ).

Its effect is to assert that the ranges of f and g are are disjoint. I.e. if f and g are declared as follows:

      f: [ sort ] -> t.
      g: [ sort ] -> t.

then the command

      disjoint( f, g ).

effectively asserts the following axiom:

      forall( [ x: sort, y: sort ], ^f(x) = g(y) ).

For reasons of efficiency, Seduct does not literally assert this axiom. The command freely generated (cf. section 7.3.24) makes the disjointness assertion for any two functions found in its second argument.

7.3.17 do not show proofs

This command takes no parameters and has the form:

      do not show proofs.

Its effect is to set the global variable show proof to false, which suppresses the graphical presentation of proofs constructed with the go command. The effect of the command is cancelled by the show proofs command (cf. section 7.3.45).

7.3.18 end( believe )

This command takes no parameters. Its syntax is

      end( believe ).

It cancels the effect of a corresponding begin( believe ) command. Both commands are described in section 7.3.6.

7.3.19 end( time )

This command takes no parameters. Its syntax is

      end( time ).

It reports the time that has passed since the corresponding begin( time ) command. The corresponding begin( time ) command is the latest for which no corresponding end( time ) command has been executed.

7.3.20 end This command takes one parameter. Its syntax is

      end( id ).

It stops the recording of commands for the definition of macro id. It is described together with the macro command in section 7.3.32 on page 84.

Note that a macro named m cannot contain the command end(m) (e.g. a macro time cannot contain an

end(time) command).

7.3.21 end of file This command takes no parameters. Its syntax is

end of file end of file is the pseudo-character at the end of a file. On most UNIX^{TM} systems, the keyboard equivalent of this is ctrl-D. In Seduct, this command can also be typed as end of file. When not recording a macro, an end of file causes Seduct to issue a warning and then attempt to execute a quit command which when reading commands form the keyboard causes an error message. When reading a macro, end of file causes an error.

Warning: Do not generate end of file from the keyboard, always end command files with a quit command, and always make sure that macro definitions are properly completed (cf. section 7.3.32).

7.3.22 execute

This command takes one parameter. Its syntax is

      execute( File ).

where File is the name of a file containing a sequence of Seduct commands. The file name has to be enclosed in quotes if it contains anything which Prolog would interpret as a variable (e.g. an atom starting with a capital letter). The command execute(File) causes Seduct to read its input from the file File until this file is exhausted. After that, control is returned to the user (or to the calling file, if the execute command was executed from a command file). execute commands may be nested, i.e. a file executed by an execute command may itself contain execute commands to execute further files. All files to be executed should be ended with a quit command. Furthermore, if a file to be executed contains a protocol command, it has to contain a close command which closes the file opened by the protocol command.

7.3.23 exit

This command takes no parameters and has the form:

      exit.

Its effect is to end a Seduct session and return to the calling program (usually a shell). All files opened for input by the execute command and any file opened for output by the protocol command are closed.

7.3.24 freely generated

This command takes two parameters. Its syntax is

      freely generated( sort, Generators ).

Here sort denotes a sort while Generators is a list of names of functions with range sort sort. The declarative meaning of the command

      freely generated( sort, [ f_{1}, · · ·, f_{n} ] )

is that the sort sort is freely generated by the constructors f_{1}, ⋯, f_{n}. A sort sort is defined to be freely generated by the constructors f_{1}, ⋯, f_{n} if and only if the following three conditions hold:

1. The sort sort is generated by the constructors f_{1}, ⋯, f_{n}.

2. For all i ∈ {1, ⋯, n} the functions f_{i} are injective.

3. For all i, j ∈ {1, ⋯, n} with i different from j the ranges of f_{i} and f_{j} are disjoint.

The last two conditions are referred to as freeness axioms. We will discuss each of the three conditions in the definition above in turn.

We start with the first condition. A sort sort is said to be generated by the constructors f_{1}, ⋯, f_{n} if every element of sort sort can be constructed from constants by a finite number of applications of the functions f_{i}. More formally, the sort sort has been constructed according to an inductive definition. To make this notion precise we have to make some assumptions about the arity declarations of the functions f_{i}. let us assume that the declaration of the ith function is given by

f_{i}: [ sort_{i1}, ⋯, sort_{ik(i)} ] -> sort

where k(i) is the arity of the ith function. Then for sort to be generated by the functions f_{i} we demand that every element of sort sort can be constructed according to the following inductive definition:

1. If for all j ∈ {1, ⋯, k(1)} the element sort_{j} is of sort sort_{1j}, then f_{1}(sort_{1},⋯,sort_{k(1)}) is of sort sort.
⋮

n. If for all j ∈ {1, ⋯, k(n)} the element sort_{j} is of sort sort_{nj}, then f_{n}(sort_{1},⋯,sort_{k(n)}) is of sort sort.

To make things concrete we discuss an example. Assume that the declarations

      arity( zero: nat ).
      arity( succ: [ nat ] -> nat ).

have been given and that there is a generation clause of the form

      freely generated( nat, [ zero, succ ] ).

This generation clause implies that every element from nat can be constructed according to the following inductive definition:

1. zero is an element of nat.

2. If n is an element from nat, then also succ(n) is in nat.

Operationally, if a sort sort is defined as being generated inductively, this makes the induction command available. This command is discussed in section 7.4.13.

Let us now discuss what is meant by demanding that the functions f_{i} generating the sort sort are injective. Assuming the declarations of the f_{i} which have been given above, this is logically equivalent to asserting for each i ∈ {1, ⋯, n} the axiom

f_{i}(x_{1},⋯,x_{k(i)}) = f_{i}(y_{1},⋯,y_{k(i)}) → x_{1} = y_{1} ∧ ⋯ ∧ x_{k(i)} = y_{k(i)}

Taking in our example from the last paragraph, we get:

      succ(x) = succ(y) → x = y

Operationally, for efficiency reasons the formulae describing the injectivity of the constructor symbols are not added directly as axioms into the system. Rather, they are hard-wired into the rewrite calculus in the following way: If a new equation of the form

      f(s_{1},· · ·,s_{k}) = f(t_{1},· · ·,t_{k})

has been produced and if f is a constructor for a freely generated sort, then instead of adding this equation to the set of rewrite rules, Seduct adds the equations

      s_{1} = t_{1}, · · ·, s_{n} = t_{n}

as new rewrite rules, after orienting them appropriately.

Finally, we discuss what is meant by demanding that different constructors have different ranges. Logically this amounts to adding the axioms

f_{i}(x_{1},⋯,x_{k(i)}) ≠ f_{j}(y_{1},⋯,y_{k(j)}) (1)

for every pair (i, j) with i different from j. In our example this would result in one axiom:

      succ(x) ≠ zero

Again these axioms are hard-wired into the rewrite calculus. If Seduct derives an equation of the form

f(s_{1},⋯,s_{k}) = g(t_{1},⋯,t_{k}) (2)

where f and g are \underline{different} constructor symbols for a freely generated sort, then the particular sequent to be proved by the rewrite calculus has been established as valid. This is due to the fact that (1) and (2) taken together are inconsistent.

For the freely generated command to be meaningful, all the constants appearing in the list Generators have to be of sort sort. The range of any function symbol appearing in this list has to be the sort sort. Furthermore, if there is no constant in the list Generators there has to be at least one function symbol in this list whose domain does not contain the sort sort. (This last condition is needed to ensure that the inductive definition defining the sort sort is well-founded.)

7.3.25 generated

This command takes two parameters. Its syntax is

generated( sort, Generators ).

Here Generators is a Prolog list of constant and function names. The intended meaning of this command is to express the fact that the sort sort is generated by the constants and functions appearing in the list Generators. To explain the notion of a sort being generated we give an example. Assume there is a sort tree consisting of binary trees labeled with natural numbers. Assume further that the following declare section is given:

      begin(declare).
         leaf: [ nat ] -> tree.
         cons: [ nat, tree, tree ] -> tree.
      end(declare).

Then executing the command generated( tree, [ leaf, cons ] ) would from a declarational point of view be equivalent to giving the following inductive definition of the sort tree:

1. For every n of sort nat, the term leaf( n ) is of sort tree.

2. If n is of sort nat and t_{1} and t_{2} are of sort tree, then the term cons( n, t_{1}, t_{2} ) is of sort tree.

This inductive definition guarantees that all values of sort tree can be constructed using the constructors leaf and cons. Therefore it enables us to prove a statement of the form forall( t: tree, F) by induction along the definition of the sort tree. An inductive proof of the statement given above consists of the following steps:

1. Prove the statement F[t ← leaf(n)], where n denotes a new constant of sort nat.

2. Prove the statement F[t ← cons(n,t_{1},t_{2})], where n denotes a new constant of sort nat and t_{1} and t_{2} are new constants of sort tree. In this proof, the validity of the statements F[t ← t_{1}] and F[t ← t_{2}] can be assumed.

Although we have only explained the generated command by an example, we hope that its meaning has become clear. For further information the reader is referred to the discussion of the freely generated command and to the discussion of the induction command.

For the generated command to be meaningful, all the constants appearing in the list Generators have to be of sort sort. The range of any function symbol appearing in this list has to be the sort sort. Furthermore, if there is no constant in the list Generators there has to be a least one function symbol in this list whose domain does not contain the sort sort.

7.3.26 goal

This command takes one parameter and has the form:

      goal( Name: F ).

Execution of this command asserts the formula F as new goal to be proved later. This goal is referred to by its name Name.

7.3.27 help

This command takes one parameter and has the form:

      help( Command ).

In a separate process, it starts up an xdvi session on this manual. The page shown initially is the one where the description of Command starts.

7.3.28 inform

This command takes one parameter. Its syntax is

      inform( Message ).

The effect of this command is to print the message Message to the screen when it is executed. If the output has been redirected by a protocol command this message is also written to the protocol file which is currently active.

7.3.29 injective

This command takes one parameter. Its syntax is:

      injective( f ).

It defines the function f to be injective, i.e. for a function with k parameters:

f( x_{1}, ⋯, x_{k}) = f( y_{1}, ⋯, y_{k}) → x_{1} = y_{1} ∧ ⋯ ∧ x_{k} = y_{k} An example of injectivity is given in section 7.3.24 describing the freely generated command.

7.3.30 instantiate

This command comes in two variants. The first variant takes three parameters. Its syntax is:

      instantiate( Name, T, New Name ).

The second variant takes four parameters. It is written as:

      instantiate( Name, x, T, New Name ).

Name must be the name of an axiom, a definition, a lemma which may be used as a definition or a theorem. The purpose of this command is to instantiate the formula F referred to by Name. This is only meaningful if F is universally quantified.

If F is a formula of the form

      forall( x: sort, G )

where x is a variable of sort sort, then the variant taking three parameters can be used. After successful completion of this variant, New Name refers to the formula G[x ← T]. This new formula is then asserted as an axiom.

The second variant is used if F takes the form

forall( [ x_{1}: sort_{1}, ⋯, x_{n}: sort_{n} ], G ). This variant is subject to the condition that the variable x is equal to one of the variables x_{i} for i ∈ {1, ⋯, n}. We need the additional parameter x in this case to specify which variable has to be replaced. Otherwise there is no difference between the first and the second variant of the instantiate command. After successful execution of the second variant of the instantiate command, the formula New Name refers to the formula

forall( [x_{1}: sort_{1}, ⋯, x_{i−1}: sort_{i−1}, x_{i+1}: sort_{i+1}, ⋯, x_{n}: sort_{n} ], G[x←T] ).

7.3.31 linear ordered

This command takes one parameter. Its syntax is:

      linear ordered( sort ).

Its effect is to assert that =< is a linear order for the sort sort, i.e. that the following axioms hold:

      x =< y

      x =< y & y =< x -> x = y
      x =< y & y =< z -> x =< z
      x =< y v y =< x

Moreover, the predicates <, >= and > are defined by:

      x > y <--> ^x =< y
      x >= y <--> y =< x
      x < y <--> ^x >= y

The axioms defining the actual order must, of course, be provided by the user.

7.3.32 macro

This command takes one or more parameters. Its syntax is:

      macro( id, P_{1}, · · ·, P_{n} ).

id is an identifier which is the name of the macro being defined, P_{1}, ⋯, P_{n} are identifiers that name the formal parameters. The formal parameter identifiers must be different from each other.

This command puts Seduct in macro definition mode where the commands are recorded without being processed. Seduct is brought back to command processing mode by means of the end(id) command. If an end command with an identifier corresponding to that in the macro command is not found, Seduct keeps recording commands until some error (e.g: end of file) causes it to crash.

The macro execution command has the syntax:

id( E_{1}, ⋯, E_{n} ).

It executes the commands recorded for macro id after replacing all occurrences of each formal parameter name P_{i} with the corresponding actual parameter string E_{i}. Thus, if a formal parameter name is used which co-incides with a Seduct command name, this command should not be used in the macro since the command name would be replaced by an actual parameter string. The problem can easily be avoided by avoiding formal parameter names that co-incide with Seduct command names.

An example of a macro definition is:

      macro( symbolic execution, goal, var, theory).
         prove( goal, theory).
           induction(var).
              expand all.
              go.
              expand all.
              go.
      end(symbolic execution).

and a call of this macro could look like this:

      symbolic execution( lemma 1, l1, []).

Notice, that the use of goal and theory as formal parameters prevents their use as commands in the macro definition.

7.3.33 monotone

This command takes one parameter. Its syntax is:

      monotone( f ).

Its effect is to assert that the function f is monotone in every argument, i.e. that if f has the signature

f: [ sort_{1}, ⋯, sort_{n} ] -> sort

then for all i ∈ 1, ⋯, n the following axiom holds:

x_{i} =< y_{i} -> f( x_{1}, ⋯, x_{i}, ⋯, x_{n}) =< f( x_{1}, ⋯, y_{i}, ⋯,x_{n})

7.3.34 op

This command takes three parameters. Its syntax is

      op( n, a, op ).

Here, n is a natural number (0 ≤ n ≤ 1200), a is an arity and associativity code, and op is a constant, function or predicate symbol. The effect of this command is to add (or delete) an operator symbol to the parsing tables.

In Prolog operator symbols can be overloaded in the sense that the same operator symbol can be used for both a unary (either prefix or postfix) and a binary operator, which may have different precedences and associativity properties. However, in Seduct this feature is of no use since there is no overloading of function names. Both arity and associativity of the operator which has been declared are indicated by the code given as parameter a. The possible values for this code and their corresponding meanings are listed in table 1.

If n is 0, the operator symbol op and the arity indicated by a is deleted. If n is greater than 0, the operator symbol op and the arity indicated by a is defined (redefined if it already exists) with a precedence of n and the associativity indicated by a. The lower the value of n, the tighter does the operator bind to its operands.

WARNING: Users of Seduct are strongly advised not to define operators of a precedence greater or equal than 700, since operators with a precedence of 700 or above might interfere with Seduct operator declarations and thereby lead to unpredictable results.

The predefined operator symbols with their precedences and arity and associativity codes are listed in table 2. This table also mentions any differences from the predefined operators of the Prolog interpreter.

The defined operator symbols can be displayed using the show(ops) command (cf. section 7.3.44).

Code  Meaning
Associativity  Arity
fx  non-associative unary prefix
fy right-associative unary prefix
xf  non-associative unary postfix
yf  left-associative unary postfix
xfx  non-associative binary infix
xfy right-associative binary infix
yfx  left-associative binary infix

Table 1: Arity and associativity codes for the op command

7.3.35 operator

This command takes two parameters. Its syntax is

      operator( f: n ).

Here n is a natural number, while f is any of the existing constant, function or predicate symbols. If the function symbol f either is an infix operator or has been declared as an infix operator, it is necessary to put f into parentheses. For example, the symbols “+” or “-” would have to be set into parentheses as in

      operator( (+): 3 ).

Prec- Associ- Operator Differences from
edence ativity symbol original Prolog operators
1  xfy  -  Original precedence: 500. Original associativity: yfx
2  xfx  .  Added.
3  xfy  /  Original precedence: 400. Original associativity: yfx
4  fx  /  Added.
200  fx  +
200  xfy  ^
500  yfx  +
700  xfx  <
700  xfx  =
700  xfx  =<
700  xfx  >
700  xfx  >=
900  fx  ^
910  xfy  &  Added.
920  xfy  v  Added.
930  xfy  ->  Original precedence: 1050
940  xfx  <-->  Added.
950  xfx  '|-'  Added.
950  xfx  :  Original precedence: 50
1000  xfy  ','
1100  xfy  ;
1200  fx  :-
1200  fx  ?-
1200  xfx  -->
1200  xfx  :-

Table 2: Predefined operator symbols

Moreover, operators containing a full stop have to be quoted since a non-quoted indicates the end of a command to the parser. For more information, see appendix A.

The effect of this command is to assign the number n to the operator op. This number is later used when it comes to comparing different operators. Comparisons of operators are made when terms are compared by the lexicographic path ordering.

7.3.36 protocol

This command takes one parameter. Its syntax is

protocol( File ).

where File is a file name. Initially, all commands executed by Seduct are protocoled in the file script. Execution of the command “protocol( File )” redirects the protocol into the file File. Commands are then no longer protocoled in the file script. Protocoling the commands to File must be ended by the close command. If a protocol command has been executed from a file which itself is executed by the execute command, then this file must contain a close command which matches the protocol command.

Like the execute command, protocol commands can be nested.

7.3.37 prove

This command takes one parameter and has the form:

prove( Name, Theory ).

This command initiates the proof of the formula referred to by Name. For this to work, Name has to refer to a goal, while Theory can can take the forms described for the theory command (cf. section 7.3.47) with the added restriction that the theory defined by Theory is not allowed to contain any unproved goal. The precise effect of this command is to create a goal stack containing a single sequent:

[A_{1}, ⋯,A_{n} ] ⊢ [F]

where [A_{1}, ⋯, A_{n}] is the list of all the formulae referred to by Theory, while F is the goal referred to by Name. After creating the goal stack the prove command switches Seduct from command mode into prove mode. Visually, this can be seen by a change in the prompt of Seduct. As long as Seduct is in command mode it prompts with the string

      SEDUCT>

In prove mode, this prompt changes to

      SEDUCT(Name):

where Name refers to the goal currently being proved.

The prove command does not actually carry out any proof. This is done by the go command, which might itself be preceded by other prove mode commands. These commands are explained in section 7.4.

7.3.38 quit

This command takes no parameters and has the form:

      quit.

The command is used to quit from the current command loop of Seduct. It is intended to be used only in command files which are executed by the execute command. If a quit command occurs in a command file, execution of this file is aborted. If the execute command invoking execution of this file had been given by the user, control is returned to him and he is prompted for further commands. If the execute command had been invoked by another command file which had itself been invoked by the execute command, control is passed back to this command file. Every command file should be ended by a quit command.

If a quit command is issued by the user, an error message is displayed.

7.3.39 remove

This command takes two parameters. Its syntax is

      remove( key, Name ).

Here key is one of the following keywords:

      axiom, definition, freely generated, generated, goal, operator precedence, theorem or theory.

Name is the name of an object which has been specified by the keyword key. This command retracts the axiom, definition, freely generated declaration, generated declaration, goal, operator precedence declaration, theorem or theory which has been laid down by the pair key and Name.

For further illustration, let us consider the following example: If there exists the definition

      definition( def: Formula ),

where Formula is a well-formed formula, then the command

      remove( definition, def )

will retract the definition named def.

This command is not available in strict mode (cf. section 7.1).

7.3.40 rewrite counter

This command takes one parameter. Its syntax is

      rewrite counter( n ).

It resets the value of the global variable rewrite counter to n, where n is a natural number. This variable controls how many times the rewrite loop is executed. The default value of this counter is 16.

7.3.41 run This command takes no parameters and has the form:

      run.

The run command is just an alias for the command execute( run ), which in turn executes the command file run. The semantics of the execute command has already been explained above. Of course, if there is no command file named run execution of the run command will result in an error.

7.3.42 set( show )

This command takes one parameter and has the form:

      set( show( key ) ).

This command causes Seduct to execute a show(key) command each time the current sequent has changed, which, of course, is only possible in prove mode. Any key that is legal for the show commands described in sections 7.3.44 and 7.4.20 can be used^{33}. The effect of this command is cancelled by the unset(show) command described in section 7.3.48.

7.3.43 set( strict )

This command takes no parameters and has the form:

      set( strict ).

This command puts Seduct into strict mode where commands that could compromise the correctness of a proof cannot be used. To leave strict mode, the unset(strict) command (cf. section 7.3.49) is used.

7.3.44 show This command takes one parameter and has the form:

      show( key ).

This command is used to control the current state of the proof. The variable key can take one of the following values:

declarations: In this case the command prints the declarations of all constants, functions and predicates

currently defined. axioms: This prints all the axioms currently available. definitions: This prints all the definitions currently available.

33Only the prove mode keys (goal and complete) make sense: The information displayed by the other keys does not usually change between commands that change the current sequent.

goals: This prints all the goals which have not yet been proved.

theories: This prints all the theories currently available.

theorems: This prints all the theorems which have been proved.

all: This prints all the information available, i.e. all declarations, axioms, definitions, goals, theories and theorems are listed.

ops: This prints all the currently defined operator symbols with their corresponding precedences and arity and associativity codes. As, the listing is rather long-winded, it is recommandable to use a window that can be scrolled backwards, if you want to use this command.

macros: This prints all the currently defined macros with their formal parameters and macro bodies.

7.3.45 show proofs

This command takes no parameters and has the form:

      show proofs.

Its effect is to set the global variable show proof to true. If this variable is true, the user gets the option to inspect a graphical presentation of proofs constructed with the go command. The effect of this command is cancelled with the do not show proofs command (cf. section 7.3.17).

7.3.46 system

This command takes one parameter and has the form:

      system( UC ).

It is used to execute operation system commands. In general, it works by creating a subshell, executing the UNIX^{TM} command UC in this subshell, and finally killing the subshell. However, there is a special case where executing this command in a subshell would be useless. This special case is the “cd” command to change the directory.^{34} Issuing a cd command will change the current directory of Seduct and not the current directory of a subshell.

Since input for Seduct has to be a legal Prolog term, it will usually be necessary to enclose UC in quotes. For example, in order to change the directory to

      /home/x2000/karl/Cases

(this is where the examples are), the following command is used:

      system( 'cd /home/x2000/karl/Cases' ).
7.3.47 theory

This command takes one parameter and has the form:

      theory( T = D ).

Its effect is to define a new theory D named T. The theory definition D is either a list consisting of axiom names, definition names, theorem names and goal names, or it is of the form

D_{1} + D_{2}

34After all, the subshell ceases to exist after execution of the UC command. Therefore, changing its current directory is not very useful.

where D_{1} and D_{2} are either theory definitions or the names of previously defined theories. If a theory contains goal names, it can only be used after these goals have been proved and, thus, turned into theorems.

7.3.48 unset( show )

This command takes no parameters and has the form:

      unset( show ).

It cancels the effect of any previous set(show(key)) command (cf. section 7.3.42), i.e. it causes Seduct to stop automatically executing a show command (cf. sections 7.3.44 and 7.4.20) after each change to the current sequent.

7.3.49 unset( strict )

This command takes no parameters and has the form:

      unset( strict ).

It causes Seduct to leave strict mode, i.e. to allow the use of commands like believe and remove (cf. sections 7.4.4 and 7.3.39, respectively.) that may compromise the correctness of a proof. The effect of this command is cancelled by the set(strict) command described in section 7.3.43.

7.4 Commands Available in the Prove Mode

7.4.1 abort

This command takes no parameters and has the form:

      abort.

This command aborts the current proof. It brings Seduct back into the state before execution of the command that generated the current sequent. Apart from a possible change in prove mode, the command interpreter modes, axioms, declarations etc. are not affected by this state change.

7.4.2 add This command takes one parameter and has the form:

      add( Theory ).

Theory has the form of a theory definition as described for the theory command in section 7.3.47. This command adds the formulae contained in the theory defined by Theory to the antecedent.

7.4.3 alpha normalize

This command takes no parameters and has the form:

      alpha normalize.

This command simplifies the current sequent using alpha rules:

\frac{Γ ⊢ Δ, P}{Γ, ^P ⊢ Δ}

\frac{Γ, P ⊢ Δ}{Γ ⊢ Δ, ^P}

\frac{Γ, P, Q ⊢ Δ}{Γ, P & Q ⊢ Δ}

\frac{Γ ⊢ Δ, P, Q}{Γ ⊢ Δ, P v Q}

\frac{Γ, P ⊢ Δ, Q}{Γ ⊢ Δ, P -> Q}

Since the alpha rules concerning quantifiers (cf. section 5.5) are not used, this command has no effect for a quantified goal. To get rid of universal quantifiers, the skolemize command (cf. section 7.4.21) can be used.

The usefulness of the alpha normalize command can be demonstrated by the following small example. If the current sequent is

A -> B = C, A & D ⊢ F(B)

then the the primitive rewriting engine of expand (and expand all) will not be able to replace F(B) with F(C) since it is not able to conclude that A holds. Using alpha normalize yields

A -> B = C, A, D ⊢ F(B)

where expand can replace B by C.

7.4.4 believe

This command takes no parameters and has the form:

      believe.

This command turns the current goal into a theorem without proving it. It can be used during the development of a proof to postpone the development of an uninteresting or complicated part of it till some later time.

This command is only available in non-strict mode.

7.4.5 beta normalize

This command takes no parameters and has the form:

      beta normalize.

This command simplifies the current sequent using the alpha rules used by the alpha normalize command (cf. section 7.4.3) and the following beta rules:

\frac{Γ ⊢ Δ, P Γ ⊢ Δ, Q}{Γ ⊢ Δ, P & Q}

\frac{Γ, P ⊢ Δ Γ, Q ⊢ Δ}{Γ, P v Q ⊢ Δ}

\frac{Γ ⊢ Δ, P Γ, Q ⊢ Δ}{Γ, P -> Q ⊢ Δ}

\frac{Γ ⊢ Δ, P, Q Γ, P, Q ⊢ Δ}{Γ, P <--> Q ⊢ Δ}

\frac{Γ, P ⊢ Δ, Q Γ, Q ⊢ Δ, P}{Γ ⊢ Δ, P <--> Q}

\frac{Γ, C, P ⊢ Δ Γ, Q ⊢ Δ, C}{Γ, if( C, P, Q) ⊢ Δ}

\frac{Γ, C ⊢ Δ, P Γ ⊢ Δ, C, Q}{Γ ⊢ Δ, if( C, P, Q)}

Moreover, simple predicate logic rewriting is performed, and trivial sequents are deleted.

Since the rules concerning quantifiers (cf. section 7.4.5) are not used, this command has no effect for a quantified goal. To get rid of universal quantifiers, the skolemize command (cf. section 7.4.21) can be used.

To get a better feeling for the functionality of the beta normalize command, here is a small example.

If the current sequent is

      Antecedent:

       (1)  forall([x : element,l2 : list], x >>= c1 & x =<< l2 -> c1 ==<< l2)
      Succedent:
       (1)  (c2 >= c3 & c2 >>= c1) & c2 =<< c4 -> c3 =<< c4 & c1 ==<< c4

then beta normalize will replace it with the following two sequents:

      Antecedent:
       (1)  c3 =< c2
       (2)  c2 >>= c1
       (3)  c2 =<< c4
       (4)  forall([x : element,l2 : list], x >>= c1 & x =<< l2 -> c1 ==<< l2)
      Succedent:
       (1)  c3 =<< c4

and

      Antecedent:
       (1)  c3 =< c2
       (2)  c2 >>= c1
       (3)  c2 =<< c4
       (4)  forall([x : element,l2 : list], x >>= c1 & x =<< l2 -> c1 ==<< l2)
      Succedent:
       (1)  c1 ==<< c4

The universally quantified formula in the antecedent is left unchanged, the left-hand side of the implication in the succedent is moved into the antecedent and the conjunction is dissolved, the right-hand side of this implication becomes a conjunction in the succedent causing the sequent to be split in two: one for each formula in the conjunction.

7.4.6 case induction

This command takes one parameter and has the form:

      case induction( x ).

It can only be used if x is a skolem constant, or if the current goal is of the form:

forall( [ x_{1}: sort_{1}, ⋯, x_{n}: sort_{n} ], F )

and x is equal to one of the variable names x_{i}.

It requires that there is a generated or freely generated clause for the sort sort of the variable x. In the following, we will assume that the current goal has one universally quantified variable, i.e. that it has the form:

      forall( x: sort, F )

and that the generated clause for the sort sort has the form:

      generated( sort, [ f_{1}, · · ·, f_{m} ] ).

In order to prove the current goal, the following rule is applied:

\frac{Premise_{1}  ⋯  Premise_{m}}{Γ ⊢ forall( x: sort, F )}

Here Γ lists the axioms of the theory from which the formula forall(x: sort, F) is to be proved. If the declaration of f_{i} has the form:

f_{i}: [ sort_{i1}, ⋯, sort_{ik} ] -> sort

where k is the arity of the function f_{i}, then Premise_{i} has the form:

Γ ⊢ F[ x ← f_{i}(c_{i1}, ⋯, c_{ik}) ]

where the c_{ij} are new constants of appropriate sorts.

Execution of the case induction command first removes the current goal from the top of the goal stack and then pushes the premises Premise_{1}, ⋯, Premise_{m} onto it. After that the premise Premise_{1} will be the current goal, i.e. the topmost goal on the goal stack. The goals corresponding to the premises are named according to the following convention: If g is the name of the current goal before execution of the induction command, the name of the goal corresponding to the ith premise will be g case ind i.

In other words, if the current sequent g is

      ⊢ forall( x: nat, zero =< x)

and there is a freely generated clause for nat of the form

      freely generated( nat, [ zero, succ ] ).
then case induction will generate two sequents g case ind 1 and g case ind 2:
      ⊢ zero =< zero
      ⊢ zero =< succ( c1 )

assuming that c1 is the first unique name that has been generated for for a skolem constant in the current proof.

7.4.7 cases

This command takes one parameter and has the form:

      cases( Case List ).

This command triggers a proof by cases. The parameter Case List is a list of formulae. If we have

Case List = [ C_{1}, ⋯, C_{n} ]

and the topmost goal on the goal stack is

Γ ⊢ F

then the effect of the command cases( Case List ) is to remove the top goal and instead push the goals

0. Γ ⊢ C_{1} ∨ ⋯ ∨ C_{n}
1. Γ, C_{1} ⊢ F
⋮
n. Γ, C_{1} ⊢ F

onto the goal stack. After the execution of the cases command, the goal Γ ⊢ C_{1} ∨ ⋯ ∨ C_{n} will be the first goal on the goal stack. If g is the name of the current goal, the name of the goal Γ ⊢ C_{1} ∨ ⋯ ∨ C_{n} will be g cases. For all i ∈ {1, ⋯, n} the goals Γ, C_{i} ⊢ F will get the name g case i.

Logically, the cases command is equivalent to the application of the following rule

\frac{Γ ⊢ C_{1} ∨ ⋯ ∨ C_{n}  Γ, C_{1} ⊢ F  ⋯  Γ, C_{n} ⊢ F}{Γ ⊢ F}

The first premise Γ ⊢ C_{1} ∨ ⋯ ∨ C_{n} simply guarantees that the case distinction is complete, i.e. that no case has been forgotten.

The intention behind offering the cases command is the observation that the proof of a conjecture can often be simplified by dividing the proof into cases. If a conjecture is a theorem which cannot be proved with Seduct, an attempted proof by cases may simplify the conjecture and thereby circumvent the incompleteness of the automatic theorem prover behind Seduct. If a conjecture is not a theorem, an attempted proof by cases might spot the case where a conjecture fails to be a theorem.

7.4.8 crunch

This command takes no parameters and has the form:

      crunch.

Like go, it tries to automatically prove the current goal using the sequent calculus and rewriting, but unlike go it does not simply report failure if the proof does not succeed. Instead, after removing the current goal from the top of the goal stack, it collects the sequents for which no further sequent calculus rules were applicable and which could not be proved by rewriting, and pushes these onto the goal stack. Interactive commands can then be used to complete the proof.

If the current goal has the name g, each goal generated by crunch will have the name g crunch i (i > 0). To determine beforehand how many goals will be generated requires a deep understanding of the inner workings of Seduct.

7.4.9 cut

This command takes one parameter and has the form:

      cut( C ).

Here C has to be a formula. This formula will be referred to as the cut formula. The command cut(C) triggers a proof by the cut rule. The cut rule is the following:

\frac{Γ ⊢ C Γ, C ⊢ F}{Γ ⊢ F}

Suppose that Γ ⊢ F is the topmost goal on the goal stack. Then the effect of the command cut(C) is to remove this goal from the goal stack and instead push the goals

1. Γ ⊢ C
2. Γ, C ⊢ F

onto the goal stack, where the first of these sequents is topmost on the goal stack afterwards. If the goal Γ ⊢ F is known under the name g, then the subgoal Γ ⊢ C will get the name g cut 1 and the subgoal Γ, C ⊢ F will be known as g cut 2.

It is well known that the cut rule can be eliminated in first-order predicate calculus. But it is also known that elimination of cuts increases the size of proofs superexponentially. Therefore, if the user has a good idea of what might be a suitable cut formula for the proof of a complicated theorem, it is advisable to use the cut rule. The cut formula C can be interpreted as a lemma valid in the theory represented by the formulae of Γ. The use of well-chosen lemmata usually results in a proof which is more perspicuous than a proof found by a brute force method.

7.4.10 expand

This command takes one parameter and has the form:

      expand( Theory ).

where Theory is a theory definition as defined in the explanation of the theory command in section 7.3.47. This command expands in the current sequent all occurrences of predicates and functions which match the left hand side of any definition or axiom contained in Theory or the left-hand side of any formula in the antecedent that has the form of a definition. A conditional definition is only considered if the validity of its condition can be established. A formula in the antecedent is not used for its own expansion as this would reduce the formulae in the antecedent to trivial equations.

Moreover, any if is reduced if the value of its condition can be established, and trivial predicate logic transformations are performed using rules like:

T = T ↔ true and

      true & F ↔ F

To make things concrete, consider the following definitions section:

      begin(definitions).
         plus s: forall( [x: nat, y: nat], x+succ(y) = succ(x+y) ).
         mult s: forall( [x: nat, y: nat], x*succ(y) = x*y+x ).
      end(definitions).

If the sequent to be proved is

      ⊢ forall( [x: nat, y: nat, z:nat], (x+y)*succ(z) = x*succ(z)+y*succ(z) )

then the command expand( [ mult s ] ) will transform this goal into the new sequent

      ⊢ forall( [x: nat, y: nat, z:nat], ((x+y)*z)+(x+y) = (x*z+x)+(y*z+y) ).

7.4.11 expand all

This command has the form:

      expand all.

This command expands occurrences of predicates and functions in the current sequent like the expand command described above (section 7.4.10). As Definition it uses all definitions defined by the definition command, all lemmata defined as definitions by the use as definition command, and all formulae in the antecedent that have the form of a definition.

7.4.12 go

This command comes in two variants. The first on takes one parameter and has the form:

go( Theory ).

It is equivalent to:

      add( Theory ).
      go.

The second form takes no parameters and has the form:

      go.

Its execution starts the automatic theorem prover embedded in Seduct, which then tries to prove the current goal. This proof search is carried out with the methods described in sections 5 and 6. In many cases, this proof search will be successful. However, due to the undecidability of first-order logic, there are cases where a proof may fail although the goal is actually correct. A proof may fail for the following reasons:

• The goal to be proved is actually false. We expect this to be the case occurring most frequently in practice. If the formula is false there may be two reasons for this:

– Although the goal is true in the intended structure, it can only be proved by induction. The reason for this may be that the goal, although being true in the intended model, is not a theorem of the first-order theory supplied by the user to axiomatize the intended structure. In this case the user has to either prove the goal by explicitly involving induction or by providing more axioms describing the intended structure.

– Another common reason for a proof search to fail is that the goal to be proved is actually false in the intended structure. After all, the whole point in doing computer aided theorem proving is to discover errors.

• Another reason a proof search may fail can be the limitation of computational resources available to the automatic theorem prover incorporated in Seduct. Again, there may be two reasons for a proof failure:

– The rewrite counter has been set too low. The default value of this counter is 16. This value can be changed by the rewrite counter command described in section 7.3.40.

– Another reason is the inherent incompleteness of the proof search of Seduct. Fortunately, the reason for this incompleteness is well known. As we have already explained in section 5, a failure of a proof search might be due to the application of a γ rule, for example if a universally quantified formula in the antecedent has been instantiated wrongly or if it has to be instantiated more than once.

If there is no goal left to prove, successful execution of the go command switches Seduct back to command mode. In any case the user can get the option to take a look at the proof constructed by the go command. If the proof is unsuccessful the proof tree will contain open leaves. Whether the proof tree is shown is controlled by the setting of the global variable show proof. If this variable is set to true by the show proofs command (cf. section 7.3.45), proofs are depicted graphically by the Motif interface.

7.4.13 induction

This command comes in two variants. The first takes one parameter and has the form:

      induction( x ).

It can only be used if x is a skolem constant, or if the current goal is of the following form

forall( [ x_{1}: sort_{1}, ⋯, x_{n}: sort_{n} ], F )

and x is equal to one of the variable names x_{i}.

The second variant takes no parameters. Its form is

      induction.

It requires that the current goal has the form

      forall( x: sort, F )

Both variants require that there is a generated or freely generated clause for the sort sort of the variable x. In the following we will only discuss the second variant of the induction command. Furthermore, we will assume that the generated clause for the sort sort has the form

      generated( sort, [ f_{1}, · · ·, f_{m} ] ).

In order to prove the current goal, the following rule is applied:

\frac{Premise_{1}  ⋯  Premise_{m}}{Γ ⊢ forall( x: sort, F )}

Here Γ lists the axioms of the theory from which the formula forall(x: sort, F) is to be proved. The premises Premise_{i} come in two forms, depending on whether the symbol f_{i} denotes a constant or a function. If f_{i} denotes a constant, then its sort must be sort. In this case Premise_{i} has the form

Premise_{i} ≡ Γ ⊢ F[x ← f_{i}].

Let us now assume that f_{i} is declared as a function and that its declaration has the form

f_{i}: [ sort_{i1}, ⋯, sort_{ik} ] -> sort

where k is the arity of the function f_{i}. For simplicity, let us further assume that the sorts sort_{i1}, ⋯, sort_{il} are equal to sort, while all the other sorts sort_{i l+1}, ⋯, sort_{ik} are different from sort. With this assumption^{35}, the ith premise will take the form

Γ, F[ x ← c_{i1}], ⋯, F[x ← c_{il}] ⊢ F[ x ← f_{i}(c_{i1}, ⋯, c_{ik}) ]

where the c_{ij} are new constants of appropriate sorts.

Execution of the induction command first removes the topmost goal from the goal stack and then pushes the premises Premise_{1}, ⋯, Premise_{m} onto it. After that the premise Premise_{1} will be the current goal, i.e. the topmost goal on the goal stack. The goals corresponding to the premises are named according to the following convention: If g is the name of the current goal before execution of the induction command, the name of the goal corresponding to the ith premise will be g ind i.

7.4.14 instantiate

This command takes two parameters. Its syntax is:

      instantiate( Name, Terms ).

Name must be the name of an axiom, a definition, a lemma which may be used as a definition, or a theorem. This command works very much like the command of the same name described in section 7.3.30. The purpose of this command is to instantiate the formula F referred to by Name. This is only meaningful if F is universally quantified. Terms is a Prolog list each element of which is either a term or the atom '?'. The length of the Terms list must be the same as the number of quantified variables in F. A single term^{36} is considered as a singleton list.

Assume that F is a formula of the form

forall( [ x_{1}: sort_{1}, ⋯, x_{n}: sort_{n} ], G ).

and, for simplicity, that Terms has the form

      [ t_{1}, · · ·, t_{k}, '?', · · ·, '?'  ]

where t_{1}, ⋯, t_{k} are terms, and the number of '?'s is n − k. Successful completion of instantiate results in the formula

forall( [ x_{k+1}: sort_{k+1}, ⋯, x_{n}: sort_{n} ], G[ x_{1} ← t_{1}, ⋯, x_{k} ← t_{k}])

being added to the current antecedent.

7.4.15 instantiate forall

This command takes two parameters. Its syntax is:

      instantiate forall( n, Terms ).

It works just like the instantiate command described in section 7.4.14, but instead of instantiating a formula referred to by its name, it instantiates the nth formula in the current antecedent.

7.4.16 instantiate exists

This command takes two parameters. Its syntax is:

      instantiate exists( n, Terms ).

35In the general case, a formula F[x ← c_{ij}] will be added to the antecedent of the premise iff the sort sort_{ij} of c_{ij} is equal to the sort sort of x.

36Actually, a single '?' is considered a singleton list, too. Such a list makes little sense, though.

It works just like the instantiate forall command described in section 7.4.15, but instead of instantiating the nth formula in the current antecedent, which much be universally quantified, it instantiates the nth formula in the current succedent, which much be existentially quantified, and adds the resulting formula to the current succedent.

7.4.17 lazy induction

This command has the form:

      lazy induction( f ).

where f is a function or predicate symbol. The following description assumes that f is function symbol. The rules for a predicate symbol f are analogous. It uses an induction principle called computational induction which in the following is briefly described, a more thorough description can be found in [2].

The current goal must consist of one universally quantified formula containing one application of the function f. The axioms defining f must be definitions, i.e., in general, each must have the form:

C_{i} -> f(A_{i0}) = F_{i}( f(A_{i1}), ⋯, f(A_{im_{i}}) ) 1≤i≤n

where n is the number of axioms defining f. F_{i} and A_{i1}, ⋯, A_{im_{i}} may not contain quantified formulae containing applications of f. For simplicity, we assume at this point that the definitions do not contain any ifs.

The definitions must form the complete definition of a total function f. Conformance with this restriction, which is not checked by Seduct, can be assured by using a specification tool like CCC ([10]).

The rule that is applied by lazy induction is:

\frac{Γ, C_{i}, G( f(A_{i1}) ), ⋯, G( f(A_{im_{i}}) ) ⊢ G( f(A_{i0}) ), 1≤i≤n}{Γ ⊢ G( f(X) )} (1)

Since f is completely defined by the above conditional equations, any possible result of an application of f will be matched by the left-hand side of one of these equations. The totality of f^{37} assures that in each equation defining f, the right-hand side (and, thus, any application of f found on the right-hand side) is less complex than the application of f which comprises the left-hand side^{38}. What the rule above says is: if we can conclude that each left-hand side of the equations defining f has a property G provided that the applications of f on the corresponding right-hand side have the same property, then all possible applications of f have this property. Since the applications of f on the right-hand side are less complex than those on the left-hand side, this is equivalent to the usual induction principle, the base cases being the left-hand sides with the lowest complexity, i.e. those where the equation does not contain applications of f on the right-hand side.

Using the definitions defining f, each succedent of the form G( f(A_{i0}) ) can be expanded into G( F_{i}( f(A_{i1}), ⋯, f(A_{im_{i}}) ) ) giving the following more useful rule.

\frac{Γ, C_{i}, G( f(A_{i1}) ), ⋯, G( f(A_{im_{i}}) ) ⊢ G( F_{i}( f(A_{i1}), ⋯, f(A_{im_{i}}) ) ), 1≤i≤n}{Γ ⊢ G( f(X) )} (2)

Let us illustrate the above with an example. If the function qs is defined by the following definitions:

   1. qs(nil) = nil
   2. forall( [ x: element, s: list],
         qs(x :: s) = qs(small part(x,s)) * x :: qs(big part(x,s))

where :: adds an element to the head of a list and * catenates two lists, and the current sequent is:

      ⊢ forall( [ l: list], ordered(qs(l)))

then the command lazy induction(qs) would, using rule (1), generate the following two sequents:

37Actually, it is sufficient that the constituent applications of f (i.e. f(X) and f(A_{ij}) (1≤i≤n, 0≤j≤m_{i})) are well-defined.

38A possible complexity measure is the number of recursions that are necessary to calculate the function value.

   1. ⊢ ordered(qs(nil))
   2. ordered( qs(small part(c1,c2)) ), ordered( qs(big part(c1,c2)) ) ⊢ ordered( qs(c1 :: c2) )

In the first sequent, the application of qs has been replaced with the left-hand side of the first axiom defining qs, i.e. qs(l) has been replaced with qs(nil). Since the first axiom defining qs contains no applications of qs on the right-hand side, the antecedent contains no additional formulae, i.e. it is empty.

In the succedent of the second sequent, qs(l) has been replaced with qs(c1::c2) which is the left-hand side of the second axiom defining qs where the universally quantified variables x and s have been replaced with skolem constants c1 and c2, respectively. Since the right-hand side of the second axiom defining qs contains two applications of qs (and since the original antecedent was empty), the antecedent consists of two formulae – each being the original succedent where one of the aforementioned applications of qs on the right-hand side of the axiom replaces the original application of qs. The quantified variables x and s have been replaced by the same skolem constants as in the succedent: c1 and c2, respectively.

These sequents could then be expanded using the axioms defining qs to give the sequents that are actually

generated by lazy induction(qs):
   1. ⊢ ordered(nil)
   2. ordered( qs(small part(c1,c2)) ), ordered( qs(big part(c1,c2)) ) ⊢
         ordered( qs(small part(c1,c2)) * c1 :: qs(big part(c1,c2)) )

Above, we assumed that the equations defining f did not contain any ifs. This restriction does not reduce the generality of the discussion since any conditional equation containing an if

      C -> E( if( Cif, F_{t}, F_{f}) )

can be replaced by two conditional equations not containing this if

      C & Cif -> E( F_{t} )
      C & ^Cif -> E( F_{f} )

To get a better idea of the effect of this command, let us look at an example. Let insert be defined by:

   1. insert( x, nil) = x :: nil
   2. insert( x, y :: s) = if( x =< y, x :: (y :: s), y :: insert( x, s))

and the current sequent be

      sorted(s) ⊢ sorted( insert( x, s))

then lazy induction(insert) will first expand the if, producing the following three equations not containing any if:

   1. insert( x, nil) = x :: nil
   2. x =< y -> insert( x, y :: s) = x :: (y :: s)
   3. ^(x =< y) -> insert( x, y :: s) = y :: insert( x, s)

and then produce the following three sequents:

   1. sorted(nil) ⊢ sorted( x :: nil)

   2. sorted( y :: s), x =< y ⊢ sorted( x :: (y :: s))
   3. sorted( y :: s), ^(x =< y), sorted( insert( x, s)) ⊢ sorted( y :: insert( x, s))

which will replace the topmost sequent on the goal stack.

7.4.18 select

This command takes two parameters. Its syntax is

select( Antecedent Selection, Succedent Selection ).

Antecedent Selection and Succedent Selection are lists of natural numbers. This command moves those formulae whose numbers are not mentioned in the selection lists from the antecedent and the succedent to the shadow antecedent and the shadow succedent, respectively. Superfluous formulae slow down the automatic proof engine (started by the go command (cf. section 7.4.12)), and might in rare cases even prevent it from proving a correct formula. In most cases, this command merely allows the automatic proof engine to produce a result a little faster.

7.4.19 select shadow

This command takes two parameters. Its syntax is

select shadow( Antecedent Selection, Succedent Selection ).

Antecedent Selection and Succedent Selection are lists of natural numbers. This command moves those formulae whose numbers are mentioned in the selection lists from the shadow antecedent and the shadow succedent to the antecedent and the succedent, respectively.

7.4.20 show

This command takes one parameter and takes one of the following forms:

   1. show( goal ).
   2. show( complete ).

It is used to display the current goal. It is especially helpful after the current goal has been expanded by the expand command or the unfold command. The first variant works only if the succedent contains a single formula, which is then displayed. The second variant prints the complete sequent to be proved. By means of the set(show(key)) command (cf. section 7.3.42), Seduct can be made to execute this command each time the current sequent has changed.

7.4.21 skolemize

This command takes no parameters and has the form:

      skolemize.

In a universally quantified current goal, it replaces the quantified variables with Skolem constants, i.e. constants whose values have not yet been established. If the current goal is not universally quantified, this command does nothing.

7.4.22 split if

This command takes no parameters and has the form:

split if.

In the current goal, split if moves ifs outwards, using the following rule:

G( ⋯, if( C, F_{t}, F_{f}), ⋯) = if( C, G( ⋯, F_{t}, ⋯), G( ⋯, F_{f}, ⋯)) and eliminates them using the following rule:

\frac{Γ, C ⊢ Δ, F_{t} Γ ⊢ Δ, C, F_{f}}{Γ ⊢ Δ, if( C, F_{t}, F_{f})}

This is done as long as the current goal contains ifs that can be moved outwards or eliminated. Quantified (sub)formulae are not affected, since subformulae of such formulae will, in general, contain quantified variables and, therefore, cannot be moved outside the scope of the quantifier.

Since split if does not operate on quantified formulae, this command has no effect for a quantified goal. To get rid of universal quantifiers, the skolemize command (cf. section 7.4.21) can be used.

Example: For the following sequent:

⊢

if( c1 =< c4, c3 =< c1 & c3 =<< small part(c4,c2), c3 =<< small part(c4,c2) ) &
if( c1 >= c4, c3 =< c1 & c3 =<< big part(c4,c2), c3 =<< big part(c4,c2) ) <-->
c3 =< c1 & c3 =<< c2

split if produces four sequents:

1. c4 =< c1,
c1 =< c4 ⊢
(c3 =< c1 & c3 =<< small part(c4,c2)) &
c3 =< c1 & c3 =<< big part(c4,c2) <--> c3 =< c1 & c3 =<< c2
2. c1 =< c4 ⊢
c4 =< c1,
(c3 =< c1 & c3 =<< small part(c4,c2)) &
c3 =<< big part(c4,c2) <--> c3 =< c1 & c3 =<< c2
3. c4 =< c1 ⊢
c1 =< c4,
c3 =<< small part(c4,c2) & c3 =< c1 &
c3 =<< big part(c4,c2) <--> c3 =< c1 & c3 =<< c2

4. ⊢

c4 =< c1,
c1 =< c4,
c3 =<< small part(c4,c2) & c3 =<< big part(c4,c2) <--> c3 =< c1 & c3 =<< c2

7.4.23 use as definition

This command takes one parameter and has the form:

      use as definition( th ).

where th is the name of a theorem, i.e. of a goal (lemma) which must have been proved. The effect of this command is to allow this theorem th to be used by the expand all command as if it were a definition. Currently, it has the further effect that th occurs in the list of definitions but not in the list of theorems as shown by the show command (cf. section 7.3.44).

For a theorem to be used as a definition, it should conform with the restrictions on definitions. Seduct does not always detect when this is not the case.

7.4.24 unfold

This command takes one parameter and has the form:

      unfold( definition ).

where definition is the of name of a definition. This command uses definition to unfold all applications of a function or predicate that match the left-hand side of definition in the current goal. It works similarly to the expand command. The only difference between the unfold command and the expand command is the fact that an unfold command takes a single definition as an argument while the expand command takes a list of definitions. Therefore, operationally the command unfold( definition ) is equivalent to the command expand( [ definition ] ). For further information the reader is referred to the explanation of the expand command.

A The Syntax of SEDUCT

This section describes the syntax of Seduct input, i.e., it describes how the scanner and the parser of Seduct work. There are two subsections. The first section describes the scanner, the second describes the parser. Since we use the scanner and the parser provided by SNI–Prolog you might also consult [12] to understand how Seduct parses its input.

A.1 The Scanner

The character set used by Seduct consists of five lexical classes:

• letters, digits, and the underscore “ ”,

• special symbols,

• forbidden symbols,

• separators,

• operator symbols. We describe each of these classes in turn.

A.1.1 Letters, Digits, and Underscore This class consists of the following symbols

    a b c d e f g h i j k l m n o p q r s t u v w x y z
    A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
    0 1 2 3 4 5 6 7 8 9
    _

Characters from this class are normally used for names of any kind, i.e., function names, variable names, predicate names, and the like.

A.1.2 Special Symbols The following symbols have a special meaning for the parser:

    , ( ) [ ] | ' %

We will explain the special meaning of each of them in turn. Comma: The comma “,” is used to separate the arguments in a term as for example in

             f(x,y).

Parentheses: The symbols “(” and “)” are used as delimiters for the arguments of terms as in

             f(x,y).

They can also be used to disambiguate the term structure when infix operators are used as in

             (x + y) * z.

Parentheses always have to come in matching pairs. Square Brackets and Stroke: The square brackets “[” and “]” and the stroke “| are part of Prolog’s short-

hand notation for lists:

             [ x_{1}, x_{2}, x_{3}, · · · | xs ]

is parsed as

             '.'( x_{1}, '.'( x_{2}, '.'( x_{3}, · · · '.'( x_{n}, xs ) · · · ) ) ).

Single Quote: The single quote “'” is used for grouping symbols from different lexical classes together. To give

an example, when confronted with the string

             =<< 1

the scanner would normally break this string into two tokens, namely “=<<” and “ 1” since the symbols “=” and “<” are from the lexical class “operator symbols”, while “ ” and “1” belong to the lexical class “letters, digits, and underscore”. In order to parse the string as a whole, we can include it in single quotes as shown below:

             '=<< 1'.

Percentage Symbol: The percentage symbol “%” is used to mark comments. As an example consider the

following input to Seduct:

             arity( plus:  [ nat, nat ] -> nat ).  % plus is used for addition

The “%” and the text following it up to the end of the line is skipped by Seduct. A.1.3 Forbidden Symbols The following symbols are forbidden, i.e., they must not be used in input for Seduct.

    ! { } ` "

These symbols are forbidden since they have a special meaning for the Prolog parser used by Seduct. A.1.4 Separator Symbols There are three white space characters that are used as separators: Blank: The blank “ ”. New–Line: The newline character. In strings it can be represented via the escape sequence “\n”. Tabulator: The tabulator character. In strings it can be represented via the escape sequence “\t”. White space characters are used to separate infix, prefix, and postfix operators from their arguments. However, they may not separate a function symbol from the left parentheses comming along with it, e.g., if f is a function symbol of three places then a string of the form

       f (x,y,z)

would be considered a syntax error. A.1.5 Operator symbols The following symbols are known as operator symbols:

    ^& = < > # * + - / : ; . ? @ \ $ ~

These symbols can be used in the same way as the symbols from the class letters, digits, and underscore, i.e., they can be used to form names. Normally they will be used to build up the names of infix, prefix, and postfix operators. Some of these symbols are already used as operators by Seduct:

• The symbols “^”, “&”, “<” “>”, and “=” are used as infix operators to build up logical formulae.

• The symbols “+”, “-”, “/” are used as operators for internal purposes.

• The backslash \ has a special meaning as an escape operator in quoted strings. Currently, the following escape sequences are available: \t: tabulator.

\n: new line. \′: single quote. \\: backslash. They can be used to include white space characters and quotes in names as in the following example:

             '\nx@\'yz'

Names of this form will not make much sense though, but nevertheless they are legal input.

• The dot “.” has been declared as an infix operator. Furthermore, it is used for the internal representation

of lists. A.1.6 Tokens Analysis When the parser of Seduct is confronted with input, two things happen in turn:

• The input stream is broken up into a list of tokens. This procedure is known as token analysis or scanning. A token is a sequence of characters that can, for example, be used as a name. Tokens are the smallest syntactical units recognizable by the parser. For this reason token are also known as atoms.

• After the scanner has converted the input stream into a list of tokens, the parser parses the list of tokens

and restructures it into a Prolog–term. This Prolog–term is then passed to Seduct. So, how does the scanner recognize a token? There are four kinds of tokens:

• Strings that start with a lower case letter and which consist solely of letters, digits and underscores.

• Strings that start with an upper case letter and which consist solely of letters, digits and underscores. These strings are interpreted as Prolog variables and may not be used in Seduct.

• Strings consisting solely of digits.

• Strings consisting solely of operator symbols.

• Arbitrary strings that are included in quotes.^{39} In order to recognize tokens, the parser tries to lump as many characters together as is admissible to produce a legal token. However, the parser always has to stop at a separator symbol. So in order to get our commands analyzed correctly, we have to separate tokens consisting of characters from the same class, e.g., if “#$” and “#” have been declared a prefix operator we would have to write

       #$ # x

instead of

       #$# x

since in the latter case, “#$#” would mistakenly be taken for a single token. On the other hand, there is no problem with writing

       #$x

since “#” and “$” on the one hand and “x” on the other hand belong to different character classes.

39Of course, these strings may not themselves contain single quotes, except escaped ones.

A.2 The Parser

After the scanner has produced a list of tokens, this list is used by the parser to build up a so called Prolog–term. It would be quite easy to describe the nature of such terms if there were no operators.^{40} Since we want to give a gentle introduction to Prolog–terms we will first present a context free grammar for Prolog–terms without operators. Terminal symbols like “,” or “|” have been included in single quotes. In the following “TOKEN” is used as a terminal symbol capable of producing any string returned as a token by the scanner during the lexical analysis.

    prolog-term  -->  TOKEN
    prolog-term  -->  "("
                       prolog-term
                       ")"
    prolog-term  -->  TOKEN
                      "("
                       prolog-term-list
                       ")"
    prolog-term  -->  "["
                       prolog-term-list
                       "|"
                       prolog-term
                       "]"

    prolog-term-list  -->  prolog-term
    prolog-term-list  -->  prolog-term
                           ","
                           prolog-term-list

There is one additional constraint which has to be mentioned at this place: It is not allowed to put white space between a token and an opening parenthesis, e.g. the string

       sin (x)

can not be parsed correctly since there is a blank between “sin” and “(x)”.

Alas, since we use operators it is not possible to describe Prolog–terms via a context free grammar. There are three types of operators which are further divided into subtypes. Each subtype can be identified through a unique identifier string, which is a string from the set {fx, fy, xf, yf, xfx, xfy, yfx}. Furthermore, every operator is equipped with a complexity, which is used to assign a priority to the operator. The complexity is a natural number between 1 and 1200. We introduce the operators together with their identifier strings in the following:

• Prefix operators can be written in front of a Prolog–term to produce a new Prolog–term, e.g., if PrefOp

is a prefix operator and PrTrm is a Prolog–term, then

PrefOp PrTrm is a new Prolog–term. To make things more concrete, if even has been declared a prefix operator, then

             even n

is a Prolog–term. There are two types of prefix operators.

40In the following, the expression “operator” is short for “infix, prefix, and postfix operator”.

– Prefix operators with associativity identifier “fx” may only be applied to terms of lower complexity than the complexity of the operator.^{41} Prefix operators with associativity identifier “fx” are called non–associative.

– Prefix operators with associativity identifier “fy” may only be applied to terms of lower or the same complexity than the complexity of the operator. Prefix operators with associativity identifier “fy” are called right associative.

• Postfix operators can be written after a Prolog–term to produce a new Prolog–term, e.g., if PrefOp is

a postfix operator and PrTrm is a Prolog–term, then

PrTrm PrefOp is a new Prolog–term. To make things more concrete, if even has been declared a postfix operator, then

n even

is a Prolog–term. There are two types of postfix operators.

– Postfix operators with associativity identifier “xf” may only be applied to terms of lower complexity than the complexity of the operator. Postfix operators with associativity identifier “xf” are called non–associative.

– Postfix operators with associativity identifier “yf” may only be applied to terms of lower or the same complexity than the complexity of the operator. postfix operators with associativity identifier “yf” are called left associative.

• Infix operators can be written between two Prolog–term to produce a new Prolog–term, e.g., if InfOp

is an infix operator and PrTrm1 and PrTrm2 are Prolog–term, then

PrTrm1 InfOp PrTrm2 is a new Prolog–term. To make things more concrete, if plus has been declared an infix operator, then

m plus n

is a Prolog–term.

There are three types of infix operators.

– Infix operators with associativity identifier “xfx” may only be applied to terms of lower complexity than the complexity of the operator. Infix operators with associativity identifier “xfx” are called non–associative.

– Infix operators with associativity identifier “yfx” may only be applied to terms of lower or the same complexity than the complexity of the operator. Additionally, the term to the right of the operator must be of lower complexity. If op is an yfx infix operator, then a string of the form

       t1 op t2 op t3

will be parsed as

       (t1 op t2) op t3.

Therefore, infix operators of this kind are called left associative.

– Infix operators with associativity identifier “xfy” may only be applied to terms of lower or the same complexity than the complexity of the operator. Additionally, the term to the left of the operator must be of lower complexity. If op is an xfy infix operator, then a string of the form

       t1 op t2 op t3

will be parsed as

       t1 op (t2 op t3).

Therefore, infix operators of this kind are called right associative.

41The notion of the complexity of a term will be introduced shortly.

Finally we have to explain the notion of the complexity of a term. Informally, this can be stated quite easily: A term has the complexity n if the term is the result of the application of an operator of complexity n, otherwise it has the complexity 0. Formally, we give the following attributed grammar for the construction of terms of complexity n. In this grammar, term(N) denotes the set of terms of complexity N, while op(N,I) denotes an operator with complexity N and type identifier I, where I ∈ {fx, fy, xf, yf, xfx, xfy, yfx}. The grammar rules are subject to side conditions which are written in curly brackets “{” and “}” below”:

prolog-term(0)  -->  TOKEN
prolog-term(0)  -->  "("
 prolog-term(N)
")"
prolog-term(0)  -->  TOKEN
"("
 prolog-term-list
 ")"
prolog-term(0)  -->  "["
prolog-term-list
"|"
prolog-term(N)
"]"
prolog-term(N)  -->  op(N,fx)
prolog-term(M)
{ M < N }
prolog-term(N)  -->  op(N,fy)
prolog-term(M)
{ M =< N }
prolog-term(N)  -->  prolog-term(M)
op(N,xf)
{ M < N }
prolog-term(N)  -->  prolog-term(M)
op(N,yf)
{ M =< N }
prolog-term(N)  -->  prolog-term(L)
op(N,xfx)
prolog-term(M)
{ L < N,  M < N }
prolog-term(N)  -->  prolog-term(L)
op(N,yfx)
prolog-term(M)
{ L =< N,  M < N }
prolog-term(N)  -->  prolog-term(L)

                         op(N,xfy)
                         prolog-term(M)
                         { L < N,  M =< N }

    prolog-term-list  -->  prolog-term(N)
    prolog-term-list  -->  prolog-term(N)
                           ","
                           prolog-term-list

Seduct offers the possibility to dynamically change the set of operators via the “op” command described in section 7.3.34. You will also find the list of all predefined operators in this section.

There is one final point worth mentioning when working with operators. Sometimes we want to use a string that has been declared as an operator as a name. The following example will explain this. Suppose the symbol “+” is to be used as the name of a theory. Then

       theory( + = [ ax1, ax2 ] ).

will not work since the parser is looking for two arguments to which it can apply the function +. The way to get around is to include the symbol + in a pair of parenthesis, e.g.,

       theory( (+) = [ ax1, ax2 ] ).

will work.

References

[1] Bachmair, L. 1991. Canonical Equational Proofs. Boston, Birkhäuser.

[2] Boyer, R. S. and J. S. Moore 1979. A Computational Logic. New York, Academic Press.

[3] Dershowitz, N. and J.–P. Jouannaud 1990. Rewrite Systems. In Handbook of Theoretical Computer Science (Vol. B: Formal Models and Semantics), pp. 243–320. Amsterdam, North–Holland.

[4] Enderton, H. B. 1972. A Mathematical Introduction to Logic. New York, Academic Press.

[5] Gallier, J. 1986. Logic for Computer Science. New York, Harper & Row.

[6] Garland, St. J., and J. V. Guttag 1991. A Guide to LP, The Larch Prover. Digital Equipment Corporation Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, Report 82.

[7] Heisel, M., W. Reif, and W. Stephan 1990. Tactical Theorem Proving in Program Verification. 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 1990. In Lecture Notes in Artificial Intelligence. Berlin, Springer.

[8] Kamin, S., and J.–J. Levy 1980. Two Generalizations of the Recursive Path Ordering. Unpublished manuscript, University of Illinois at Urbana–Champaign.

[9] Knuth, D. E., and P. B. Bendix 1970. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, pp. 263–297. Oxford, Pergamon Press.

[10] Müller, M. 1993. CCC – User’s Guide. Internal Report. Siemens AG.

[11] Smullyan, R. M. 1968. First Order Logic. Berlin, Springer.

[12] PROLOG V3.0 Sprachbeschreibung. Siemens Nixdorf Informationssysteme AG.