ndl-tutorial
28 pages
English

ndl-tutorial

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
28 pages
English
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

Natural Deduction LanguageKonstantine ArkoudasAugust 7, 2004Contents1.1 What is NDL? . . . . . . . . . . . . . . . . . . . . . . . . . . 11.2 Installing NDL . . . . . . . . . . . . . . . . . . . . . . . . . . 31.3 Interacting witn NDL . . . . . . . . . . . . . . . . . . . . . . 31.3.1 Using the GUI . . . . . . . . . . . . . . . . . . . . . . 31.3.2 Using NDL in batch mode . . . . . . . . . . . . . . . . 41.3.3 Loading files from the GUI . . . . . . . . . . . . . . . . 41.4 Input phrases . . . . . . . . . . . . . . . . . . . . . . . . . . . 41.5 NDL scripts. . . . . . . . . . . . . . . . . . . . . . . . . . . . 51.6 Signature declarations . . . . . . . . . . . . . . . . . . . . . . 51.7 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.8 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.9 Proof syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81.10 Proof semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 111.10.1 The assumption base . . . . . . . . . . . . . . . . . . . 111.10.2 Rule applications . . . . . . . . . . . . . . . . . . . . . 121.10.3 Rules dealing with equality . . . . . . . . . . . . . . . 151.10.4 Composite proofs . . . . . . . . . . . . . . . . . . . . . 161.10.5 Conditional proofs . . . . . . . . . . . . . . . . . . . . 171.10.6 Proofs by contradiction . . . . . . . . . . . . . . . . . . 171.10.7 Conclusion-annotated proofs . . . . . . . . . . . . . . . 181.10.8 ...

Sujets

Informations

Publié par
Nombre de lectures 19
Langue English

Exrait

Natural
Deduction
Language
Konstantine Arkoudas
August
7,
2004
Contents
1.1 What isNDL? . . . . . . . . . . . . . . . . . . . . . . . . . .1 1.2 InstallingNDL. . . . . . . . . . . . . . . . . . . . . . . . . .3 1.3 Interacting witnNDL. . . . . . . . . . . . . . . . . . . . . .3 1.3.1 Using the GUI . . . . . . . . . . . . . . . . . . . . . .3 1.3.2 UsingNDL. . . . . . . . . . . . . . . in batch mode .4 1.3.3 Loading files from the GUI . . . . . . . . . . . . . . . .4 1.4 Input phrases . . . . . . . . . . . . . . . . . . . . . . . . . . .4 1.5NDL. . . . . . . . . . . . . . . . . . . . . . . . . . . scripts .5 1.6 Signature declarations . . . . . . . . . . . . . . . . . . . . . .5 1.7 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 1.8 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 1.9 Proof syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 1.10 Proof semantics . . . . . . . . . . . . . . . . . . . . . . . . . .11 1.10.1 The assumption base . . . . . . . . . . . . . . . . . . .11 1.10.2 Rule applications . . . . . . . . . . . . . . . . . . . . .12 1.10.3 Rules dealing with equality . . . . . . . . . . . . . . .15 1.10.4 Composite proofs . . . . . . . . . . . . . . . . . . . . .16 1.10.5 Conditional proofs . . . . . . . . . . . . . . . . . . . .17 1.10.6 Proofs by contradiction . . . . . . . . . . . . . . . . . .17 1.10.7 Conclusion-annotated proofs . . . . . . . . . . . . . . .18 1.10.8 Quantifier reasoning . . . . . . . . . . . . . . . . . . .18 1.11 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . .21
1.1 What is NDL? NDL(Natural Deduction Language) is a formal language for expressing “Fitch-style” natural-deduction proofs [3] in first-order logic with equality. The proofs are machine-checkable.NDLis a “formal” language in that it has
1
a formal syntax, and, more importantly, a formal semantics. The semantics are given in Plotkin’s SOS1style and are centered around the notion of assumption bases, which is the hallmark of a whole family of proof languages known as DPLs (Denotational Proof Languges) [1].NDLis a simple DPL2 for first-order logic. An assumption base is just a set of premises—a set of statements that we take for granted for the purposes of the proof. This is traditionally known in logic as a “context,” a notion that has been around for a while, in particular in connection with sequent systems, where the basic unit of inference is a pair (β, Fconsisting of a context and a conclusion.)  is novel about DPLs What is that the formal meaning—denotation—of a DPL proof is specifiedrelative to a given assumption base (context). That is,the meaning of a DPL proof is a function over assumption bases, in the same way that in denotational semantics the meaning of an imperative program is a function over stores. This turns out to be an apt viewpoint that is particularly conducive to giving a rigorous semantics to Fitch-style natural deduction. Unlike sequent sys-tems, where the manipulation of the context is explicit and burdens the user, the manipulation and threading of the context in systems such asNDLis implicit and relegated to the underlying semantics—again, much as the ma-nipulation and threading of the store in imperative languages is hidden from the user. In a DPL, every proof has a unique formal meaning. If the proof is sound, then its meaning is the conclusion established by the proof; if the proof is unsound, then its meaning iserror. To obtain that meaning, weevaluate the proof in a given assumption base. Evaluation will either produce the advertised conclusion, which will verify that the proof is sound, or else it will generate an error, which will indicate that the proof is unsound. Thus in DPLs evaluation is tantamount to proof checking. InNDL, in partic-ular, evaluation—and hence proof-checking—is guaranteed to terminate in quadratic time in the length of the proof (in the worst case). This tutorial pertains to a graphical Java-based implementation ofNDL. Versions are available for Windows, Linux, and the Mac operating systems. They can be obtained from theNDLweb page: www.cag.lcs.mit.edu/~kostas/dpls/ndl and distributed in accordance with GPL, the copyright licence of GNU. 1“SOS” stands for “structured operational semantics.” 2Technically,NDLis a type-αDPL [2]. 2
1.3.2 Using NDL in batch mode It is not necessary to use the graphical interface ofNDL one. Instead, can invokeNDL Let’s assume that the currentin so-called “batch mode.” directory is theNDLdirectory (c:\ndlin a Windows system, or~/ndlin a Unix system). Then if filefoocontains aNDLscript (see section 1.5), then typingndl fooat a DOS prompt (or./ndl fooat a Unix prompt) will load the filefoo, process the variousNDLphrases in it sequentially, and display the results to the standard output device (usually the screen). The user can choose to redirect the output to a file instead of the screen by specifying a second file name as the last command-line argument toNDL, as inndl foo.in foo.out. Note that any previous contents offoo.outwill be lost.
1.3.3 Loading files from the GUI Another way to process the contents of an entire file containing a NDL script is to chooseLoadfrom theFileoption of the main menu, and then use the graphical interface to browse your directory and select the appropriate file. Loading a file has the effect of opening up the file and processing all the phrases contained in it sequentially, sending the results to the output text area.
1.4 Input phrases An inputphraseis one of the following: 1. AdeductionD . Thesyntax and semantics of deductions will be covered in Section 1.9 and Section 1.10, respectively. (Terminological note: in this document the terms “deduction” and “proof” will be used inter-changeably.) 2. Asignature declaration. These are covered in Section 1.6. 3. Anassertionis simply a string of the form . This assertF1, . . . , Fn where eachFiis aformula(formulas are discussed in Section 1.8).
4
The negation sign ˜ binds tighter than all other four connectives. Con-junctions and disjunctions have equal precedence, bind tigher than con-ditionals and biconditionals, and associate to the right. Conditionals and biconditionals have equal precedence and associate to the right. Accordingly, A & ~B \/ C ==> D & E is parsed as [A & ((~B) \/ C)] ==> [D & E] To override these conventions, use parentheses or square brackets. 3. A quantified formula is either of the form(forallx F)(auniversal quantification); or(existsx F)(aexistential quantification) for any variablexand formulaF can also be used for grouping, so. Brackets we can write[existsx F]instead of(existsx F). We will use the lettersFandGas typical formulas. We assume the reader is familiar with notions such as free and bound variable occurrences. These are defined in the standard way. Two formulas are said to bealphabetically equivalentiff each can be obtained from the other by consistently renaming bound variables. Alphabetically equivalent formulas will be viewed as identical. We writeF[x7→t] to denote the formula obtained fromFby replacing every occurrence ofxin it by the term t, renaming bound variables if necessary in order to avoid variable capture.
1.9 Proof syntax The following grammar describes the syntax ofNDLproofs: D::=RuleApp|assumeF D|p-pesboausdusrF D|D1;D2 |FBYD|beginDend |pick-anyx D |pick-witnesswfor (existsx F)D |specialize (forallx F) witht |ex-generalize (existsx F) fromt |congf(s1,...,sn) =f(t1,...,tn) froms1=t1,...,sn=tn = |rel-congR(t1,...,tn) fromR(s1,...,sn),s1=t1,...,sntn
8
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents