Index

Symbols

(-)bound: 1.4.1 Lambda-Abstraction

(semantic) tableaux: 5.2.1 Tableaux for Theorem Proving

-abstraction: 1.4.1 Lambda-Abstraction

-conversion: 1.4.8 [Sidetrack:] Alpha-Conversion

-equivalent: 1.4.8 [Sidetrack:] Alpha-Conversion

-equivalent: 3.2.10 Sidetrack: Predicates versus Functions

-reduction: 1.4.2 Reducing Complex Expressions

-structure: 3.2.6 Describing Lambda-Structures

A

abstracted over: 1.4.1 Lambda-Abstraction

atomic formula: 1.2.3 Building Formulas

B

binding edge: 3.2.5 Formulas are trees!, 3.2.6 Describing Lambda-Structures

bound variable: 1.2.4 Bound and Free Variables

C

calculus: 5.1.9 Calculi

Choice Rule: 4.2.1 The Choice Rule

closed: 5.2.3 Summing up

combinatorial explosion: 3.1.8 The Problem with the Traditional Approaches

complete: 5.1.9 Calculi

computation tree: 6.1.5 An Example - first Steps

confluence: 1.4.3 Using Lambdas

conjunctive expansion: 5.2.1 Tableaux for Theorem Proving

constant symbol: 1.2.1 Vocabularies

constraint graph: 3.2.6 Describing Lambda-Structures

constraint solving: 3.2.4 The Masterplan

conversational implicature: 5.2.5 An Application: Conversational Maxims

conversational maxim: 5.2.5 An Application: Conversational Maxims

cooperative principle: 5.2.5 An Application: Conversational Maxims

Cooper Storage: 3.1.7 Other Traditional Solutions

correct: 5.1.9 Calculi

D

deduction theorem: 5.1.8 Valid Arguments

describe: 3.2.8 Relating Constraint Graphs and Lambda-Structures

disjunctive: 5.2.2 Tableaux for Theorem Proving (continued)

Distribution Rule: 4.2.1 The Choice Rule

domain: 5.1.1 Models

dominance edge: 3.2.6 Describing Lambda-Structures

E

Enumeration: 4.1.1 Satisfiability and Enumeration

F

first-order language: 1.2.2 First-Order Languages

free variable: 1.2.4 Bound and Free Variables

functional application: 1.4.2 Reducing Complex Expressions

I

inference: 5.1.8 Valid Arguments

initial tableaux: 5.2.3 Summing up

interpretation: 5.1.4 Interpretations and Variant Assignments

interpretation function: 5.1.1 Models

K

Keller Storage: 3.1.7 Other Traditional Solutions

L

literals: 5.2.3 Summing up

M

Manner: 5.2.5 An Application: Conversational Maxims

matrix: 1.2.3 Building Formulas

meaning representation: 1.1 Introduction

model for a vocabulary: 5.1.1 Models

N

name: 1.2.1 Vocabularies

Nested Cooper Storage: 3.1.7 Other Traditional Solutions

normal dominance constraints: 3.2.4 The Masterplan, 3.2.9 Sidetrack: Constraint Graphs - The True Story

normalization: 4.2.2 Normalization

O

open: 5.2.3 Summing up

P

parent normalization: 4.2.2 Normalization

predicate symbol: 1.2.1 Vocabularies

proof: 5.1.9 Calculi

proof theory: 5.1.9 Calculi

provable: 5.1.9 Calculi, 5.1.9 Calculi, 5.1.9 Calculi

Q

Quality: 5.2.5 An Application: Conversational Maxims

quantifier store: 3.1.7 Other Traditional Solutions

quantifying in: 3.1.5 Montague's Approach to the Scope Problem

Quantity: 5.2.5 An Application: Conversational Maxims

R

redundancy elimination: 4.2.2 Normalization

Relation: 5.2.5 An Application: Conversational Maxims

relation symbol: 1.2.1 Vocabularies

restriction: 1.4.3 Using Lambdas

S

Satisfiability: 4.1.1 Satisfiability and Enumeration

saturated: 5.2.3 Summing up

scope: 1.4.3 Using Lambdas, 1.2.3 Building Formulas

scope ambiguity: 3.1.1 What Are Scope Ambiguities?

semantic construction: 1 Semantic Construction

sentence: 1.2.4 Bound and Free Variables

sign: 5.2.1 Tableaux for Theorem Proving

signature: 5.1.1 Models

signed: 5.2.1 Tableaux for Theorem Proving

solution: 3.2.8 Relating Constraint Graphs and Lambda-Structures

solved form: 4.1.4 Defining Solved Forms

sound: 5.1.9 Calculi

syncategorematically: 2.4.3 ``Special'' Words

syntactic structure: 1.3.2 Being Systematic (II)

T

tableaux inference rules: 5.2.3 Summing up

tableaux proof: 5.2.3 Summing up

tableaux refutation: 5.2.3 Summing up

term: 1.2.3 Building Formulas

theorem: 5.1.9 Calculi

true in a model: 5.1.6 Truth in a Model

V

valid: 5.1.9 Calculi, 5.1.9 Calculi

valid argument: 5.1.8 Valid Arguments

valid formula: 5.1.7 Validities

valid sentence: 5.1.7 Validities

variant: 5.1.4 Interpretations and Variant Assignments

vocabulary: 5.1.1 Models

W

well-formed formula: 1.2.3 Building Formulas

X

x-variant: 5.1.4 Interpretations and Variant Assignments