abstracted overWhen forming an abstraction, the variable in the λ-prefix is abstracted over.
admissible Calculi: An additional rule is admissible in a calculus that is already sound and complete if that rule doesn't make the calculus incorrect or incomplete.
anaphoric pronounAnaphoric pronouns are pronoun that refer back to textual antecedents.
antecedent Calculi: The antecedents (also called premises) of a rule of a calculus are those formulas that must already have been derived for the rule to be applicable. In standard notation, they are written above the bar in inference rule schemata.
argument type A version of λ-calculus where expressions are associated with types. These types enter into the well-formedness conditions of λ-expressions. They regulate how expressions can be used to form applications, and thereby make sure well-formed applications are always fully β-reducible. Moreover, they can be used to structure a functional domain when giving an interpretation to λ-calculus.
assumption Assumptions are formulae that are already given (so to speak as input) before the construction of a proof starts, and to which the rules of the respective calculus may be applied right from the beginning of the proof construction.
atomic formulaAtomic formulae are formulae that do not contain any connectives.
axiomFormulas that need not be derived from others, but can be taken for given in any proof, at any time. Using the standard inference rule notation, this can be expressed by giving for each axiom an inference rule without antecedents, with only the respective axiom as conclusion.
axiomatic method DEFINITIONDUMMY axiomaticmethod
binding edgeAdditional edges used to indicating variable bindings in the λ-structure tree notation for λ expressions in CLLS.
bound variable A quantifier is said to bind the variable standing immediately to its right. Within a quantification of the form xϕ or xϕ all occurences of x within ϕ are bound by the leading (resp. ) if ϕ itself does not contain any quantifiers. Otherwise, only those occurences are bound by the leading quantifier that are not bound by any quantifier within ϕ itself. For a more explicit formal definition of bound and free variable, see the main text.
Calculemus!"Let us calculate!" This way, the 18th century German philosopher Gottfried Leibniz expressed the hope to provide a method that would allow people to settle their differences by putting their problems in a formal language (lingua universalis) and then finding out who is right by mechanically applying a simple system of formal rules (calculus ratiocinator).
calculus A set of formal rules for manipulating items of some formal language, operating only on their syntactic structure. In logics, calculi are used to define (a.o.) the notions of proof and derivation. If a calculus is sound and complete with respect to the semantics of a logic, it can be used to prove the (semantic) validity of formulae in that logic.
calculus ratiocinator The set of rules to be used by the disputants in Leibniz' calculemus-scenario to settle their differences by purely formal calculation.
chaining ruleTableaux calculi: Additional admissible rule in tableaux calculi to allow the direct derivation of the consequent of a conditional on a branch where that conditional is found together with its antecedent.
characteristic functionFunction that decides set membership: the characteristic function of a set yields true if applied to any of the members of that set, and false for each non-member.
Choice RuleCLLS: Rule that allows for two alternative resolutions of certain CLLS-dominance constraints. (Same as Distribution Rule)
closedA tableaux is closed iff it contains at least one pair of contradictory literals on each of its branches.
combinatorial explosionCombinatorial explosion occurs when when solving a problem where a huge number of possible combinations are created by increasing the number of entities which can be combined. If one does not find a way of solving the problem without having to consider all possible combinations, solving a problem that leads to combinatorial explosion generally becomes computationally too expensive very soon.
completeA calculus is called complete with respect to a chosen semantics of its underlying language iff all formulas that are valid according to that semantics are also provable in the calculus.
computation treeA computation tree visualizes the course of the proof search conducted by a prolog program on a given input.
conclusion The conclusion of an inference rule is the formula that can be derived using that rule. In standard notation, it is written below the bar in the rule schema.
confluence Property of calculi: A calculus is called confluent if the order of rule application has no influence on the results obtained.
conjunctive expansion Tableaux calculi: An expansion by which two (or more) formulas are added to the same branch of a tableaux, and no new branches are created, is called a conjunctive expansion.
constant symbolFirst Order Logic: Syntactic entities corresponding to names: Symbols to which one fixed entity from the domain of the model in use is assigned..
constraint graph Constraint graphs are uses in CLLS to give underspecified representations of sets of λ-structures using dominance edges to record partial scoping information.
constraint solving Generally, constraint solving is the process of systematically producing one or more solutions that satisfy a set of constraints. In CLLS, constraint solving is the stepwise transformation of a constraint graph with dominance edges into a set of constraint graphs without dominance edges that - taken together - describe the same set of λ-structures as the original constraint graph. In effect, constraint solving is thus the process of producing many scopally fully specified meaning representations out of one underspecified one.
contradiction-freeModel-generation: A set of literals is contradiction-free if it doesn't contain literals AT and AF at the same time.
conversational implicatureIntentions and assumptions presumed to be present on the side of a speaker who violates any of the conversational maxims. Generally, conversational implicatures are to be inferable from the nature of such violations.
conversational maximSpecific maxims subsidiary to the general cooperative principle assumed to be followed by participants in a conversation.
cooperative principlePrinciple characterising conversation as a rational cooperative activity. According to H.P. Grice this principle, and more specifically the conversational maxims to which it leads, are normally followed by all participants in a conversation. Deviations from the principle generally allow to infer backwards to the potential assumptions or intentions of the speaker that may have caused them.
Cooper storageCooper storage is an early approach to dealing with quantifier scope ambiguities in λ-based semantic construction. It associates so called quantifier stores with semantic representations. λ-expressions for NPs can be put in the quantifier store. Different scoping constellations are then produced by applying elements from the quantifier stores at various later points in the semantic contruction process.
correctA calculus is called correct with respect to a chosen semantics of its underlying language iff all formulas that are provable in the calculus are also valid according to that semantics.
d-compositionalityCompositionality on the level of semantic interpretation, as opposed to the level of semantic representation: There is a semantic interpretation for each part of a complex expression on its own, and the interpretation of the complex expression is calculated as a function of the interpretations of the parts.
decision procedureA procedure that calculates the characteristic function of some set in a finite time. For instance a decision procedure for provability in some calculus calculus in a finite time for ech formula of the underlying language of that calculus whether is provable or not.
deduction theoremTheorem relating logical consequence and the object language conditional. E.g. the deduction theorem for propositional logic is: PQ,PQ
derivabilityCalculi: The derivability relation in a given calculus holds between a set of formulae and a single formula if there exists a proof for the single formula from the set of formulae in that calculus.
derived ruleRules that abbreviate longer subsequences of rule applications in a calculus. Derived rules are always admissible.
describe CLLS: A constraint graph describes a λ-structure if it's possible to embed the tree fragments it consists of into the λ-structure.
discourseA discourse can be taken to be a sequence of sentences. This is the simple definition adopted in most of this course. Various interesting phenomena arise when one combines sentences in a discourse, such as anaphora, presupposition, or rhetorical structure.
discourse referentDiscourse referents are entities mentioned in the discourse which pronouns potentially can refer to. They are written in the top part of a DRS, above the conditions on them.
Discourse Representation Structure (DRS)Discourse Representation Structures (DRSs) are the semantic representations used by DRT. They describe the objects mentioned in a discourse and their properties. Their structural properties amongst others allow for a sophisticated treatmentent of discourse anaphora.
Discourse Representation Theory (DRT)Discourse Representation Theory (DRT) is a theory of discourse interpretation that allows to model many phenomena that occur in multi-sentence discourses by using an intermediate level of representation. It was proposed in the early 1980s by Hans Kamp. The invention of DRT led to a shift from a static to a dynamic view on natural language semantics. To explain certain discourse phenomena, such as the interaction between indefinite noun phrases and (anaphoric) pronouns in texts shown before, the traditional account of considering meaning in terms of truth conditions turned out to be unsatisfactory. DRT adopts the rather `dynamic' view of natural language semantics, where the meaning of a sentence is defined in how it can change the context.
disjunctiveTableaux calculi: An expansion by which at least one new branch is added to a tableaux is called a disjunctive expansion.
Distribution RuleRule that allows for two alternative resolutions of certain CLLS-dominance constraints. (Same as Choice Rule)
domain First element of a model. The set that contains the entities underlying the relations and properties talked about in the language the model is for.
dominance edgeCLLS: Dominance edges are edges indicating underspecified scoping in constraint graphs. Usually drawn as dotted lines.
donkey sentenceSentences like Every farmer who onws a donkey beats it, exhibiting an interplay of quantification, conditional and anaphora that FOL-based static semantic theories are unable to capture. (Incidentally, the sentences that led to increased study of anaphoric pronouns in discourse in formal semantics, due to Peter T. Geach, staged as main characters donkeys and farmers like the example above - hence the name donkey sentences.)
enumeration Generally: The process of producing, one by one, all solutions for a given problem. In CLLS: The process of computing, given a constraint graph, all λ-structures into which it can be embedded.
exact modelA model is an exact model for a given language if for each entity in its domain, there is exactly one constant in the language.
existentialThe rule for the existential quantifier in tableaux calculi is also called the existential rule.
fairnessA tableaux expansion algorithm is called fair if every multiply expandible formula gets expanded equally often in the limit.
finite model propertyA logic is said to have the finite model property iff for every satisfiable formula, there is a finite model (i.e. one with a finite domain).
first-order formulaSyntactic entitities of first order logic that are assigned truth-values in a given model.
first-order languageSet of formulae that can be formed from a given vocabulary, a countably infinite collection of variables and a set of non-logical symbols according to the syntax rules of first order logic.
first-order modelA pair of a set of entities (the domain) and a function (the interpretation function) that assigns to each non-variable non-logical symbol of a given language an entity from, a subset of, or an n-ary relation over the domain according to the logical character of that symbol.
first order tableaux
free variableVariables (in well formed expressions) that are not bound. For an explicit formal definition of the concepts of bound and free variable, see the main text.
functional applicationThe concatenation of a λ-prefixed expression with its argument (additionally marked by an @-symbol in our notation)
Herbrand baseThe set of all constant symbols of a language.
Herbrand modelA model for a language that has as its domain the Herbrand base of that language.
inferenceFOL: The process of deriving further formulae from a given set of formulae according to rules (i.e. in a calculus). Ideally, the calculus is such that the derived formulae are logical consequences of the given ones. In this case, inference is a model of logical reasoning.
inference systemA calculus.
initial tableauxTableaux calculi: A tableaux containing only a (negated) conjecture and possibly (positive) world knowledge.
instanceCalculi: The result of substituting actual formulas for schematic letters in Axiom schemata.
interpretationThe interpretation of a term τ from a language in a model (D,F) for under a variable assignment g (written as IFg is F(τ) if τ is a constant symbol, and g(τ) if τ is a variable.
interpretation functionSecond element of a first-order model. A function assigning an element from the domain to each non-variable, non-logical symbol of the language under consideration.
iterative-deepeningGenerally: Technique of exploring a search space up to a certain depth limit, that is then augmented step by step. With each augmentation, all of the work done in the previous step is repeated. For exponentially growing search spaces, this is not a problem though, because the new part of the search space that has to be explored due to the augmentation of the depth-limit is always much larger than the part that is repeated. In this course, the technique of iterative deepening is employed when expanding universal quantifiers in the tableaux construction-algorithm.
Keller storageA revision of Cooper storage that solves some obvious problems with the original approach. (Same as Nested Cooper storage)
lexical semanticField of research that studies relations between and structures of meanings of single words.
lingua universalisLanguage that Leibniz envisaged to be used by people to formulate their problems so that they become automatically decidable, following his motto "Calculemus!" .
literalAtomic formulae and negated atomic formulae
logical constantA symbol that is neither interpreted by the interpretation function nor by the variable assignment, but whose meaning is specified implicitely in the truth condtions given for a language. A calculus has to contain rules for each logical constant of a language (leaving aside interdefinability).
mannerOne of the conversational maxims assumed by Grice. It is stated as follows: Be relevant.
matrixFormula from which a quantification is formed.
meaning constructionGiven a sentence, how do we get to its meaning? And how can we automate this process? This is the task of semantic or meaning construction.
mental modelSome cognitive theories assume that there are structured representatios underlying thought and belief in human minds. Such structures are often called mental models. When talking about model generation in this course, we take sets of literals as a scientific simplification of mental models.
model generationInference process that derives from a formula a set of literals specifying a model for that formula.
model generation procedureAlgorithm for model generation.
modus ponensInference pattern by which, given a conditional and its antecedent, the consequent is derived.
nameFOL: same as constant symbols.
negativeCalculi: Negative calculi are test calculus.
negative calculusCalculus in which a proof is constructed by showing that the negation of the conjecture is unsatisfiable.
Nested Cooper storageSame as Keller storage.
normal dominance constraintFormal language used for giving underspecified descriptions of λ-expressions. Equivalent linear notation for constraint graphs.
normalizationCLLS: Deterministic steps in the process of solving dominance constraints.
normal modelA class of models for logics that contain an equality symbol. Those models in which the equality symbol is in fact interpreted as meaning equality, i.e. τ1=τ2 is true in a normal model (D,F) iff IFg(τ1) is the same as IFg(τ2).
openA branch of a tableaux is called open iff it contains no contradictory literals. Alternatively, one can have a rule that derives a special symbol (such as ) from any pair of contradictory literals and count a branch as open iff it doesn't contain that special symbol. A tableaux is called open iff it contains at least one open branch.
parent normalizationCLLS: Normalization step in solving dominance constraints, by which dominance edges are moved towards the roots of "solid" tree fragments.
PLNQ"Predicate Logic with No Quantifiers" . Quantifier free fragment of predicate logic (therefore equivalent to propositional logic) used in parts of this course.
predicate symbolFOL: Symbols used to formalize words for properties.
premise The premises (also called antecedents) of a rule of a calculus are those formulas that must already have been derived for the rule to be applicable. In standard notation, they are written above the bar in inference rule schemata.
pronounPronouns are words that refer to objects in the text or situation in which they are uttered. In this course we mainly consider the personal pronouns he, she and it.
proofSequence of rule applications in a calculus conforming to additional conditions and starting from one formula symbolizing a conjecture. The sequence is taken to show that the conjecture formalized in the initial formula is valid.
proof from the assumptions in ℋProof that may contain formulas from a set of assumptions.
proof theoryProof theory defines calculi for given a logic and relates them to the semantically defined notions of that logic, e.g. the notions of validity and valid argument.
provabilityProperty of being provable.
provableA formula is provable in a given calculus if a proof for it can be constructed in that calculus.
provable from the assumptions in ℋA formula is provable from the assumptions in iff there is a proof from the assumptions in for it.
qualityOne of the conversational maxims assumed by Grice. It is stated as follows: Try to make your contribution one that is true.
quantifier storeStructure used by the semantic construction technique of Cooper storage to store semantic representations of NPs for later application.
quantifying inMontague's attempt to solve the problem of scope ambiguities within his framework. He postulates mutiple alternative syntactic analyses of sentences with scope ambiguities. Such analyses may employ so-called "pronouns" to delay the application of quantifiers, thereby modelling different readings of the analysed sentence.
quantityOne of the conversational maxims assumed by Grice. It is stated as follows: Make your contribution as informative as is required.
redundancy eliminationNormalization step in solving dominance constraints, by which redundant dominance edges are removed, i.e. ones that express dominances that are already expressed by (combinations of) other edges.
refutation proofA proof that procedes by refuting the negation of the original conjecture, i.e. by showing that this negation is unsatisfiable.
relationOne of the conversational maxims assumed by Grice. It is stated as follows: Be perspicuous
relation symbolFOL: Syntactic entities used to formalize words for properties and relations.
result typeType of the result of a functional application. Needs to be specified when constructing the respective functional type.
satisfiabilityCLLS: A dominance constraint is satisfiable if there is at least one λ-structure into which it can be embedded.
saturatedA tableaux is said to be saturated if no rule can be applied to any of the formulae on it producing a new result.
s-compositionalityCompositionality on the level of semantic representations: The semantic representation for a complex expression must be constructed from the semantic representations for its constituent parts in a systematic way.
scopeFormula to which a universal quantifier and a quantified variable are prefixed when forming a quantification. Same as matrix.
scope ambiguitySemantic ambiguity in an expression that can be explained by the possibility of various orderings of quantifiers or other scope-taking elements in the semantic representation of that expression.
semantic construction DEFINITIONDUMMY semanticconstruction
semi-decidableA property is semi-decidable if there exists an algorithm for checking for that property that either halts at least in all cases where the property holds, or at least in all cases where the property doesn't hold, and returns the correct result whenever it halts.
sentenceFOL: A first-order formula without any free variables.
signatureFOL: same as vocabulary.
signedCalculi: Some (tableaux) calculi use signed formulae, that is formulae to which an intended truth value is annotated, for instance in the for of a superscript T or F. Such signs can be thought of as instructions to try to make a formula true or false, respectively. Calculis that work with signed formulae are often called signed themselves.
signed formulaeSee signed.
simply typed λ-calculusVersion of λ-calculus where types pre-specifying reducible applications enter into the wellformedness conditions.
skolem constantA new constant symbol that is introduced when expanding an existential quantification.
solutionCLLS: A λ-structure is a solution of a constraint graph if the constraint graph describe that λ-structure.
solved formCLLS: A constraint graph is in solved form if it has no cycles that use only solid and dominance edges, and none of its nodes has two incoming edges that are solid or dominance
soundCalculi: Same as correct.
specificationListing of literals used to represent a Herbrand model. It contains all literals that are true in the model, all others are assumed to be false.
subformulaFOL: part of a formula that is itself a formula according to the syntax of FOL.
subordinationStructural notion in DRT capturing the accessibility of discourse referents for anaphoric reference in terms of nesting of DRSs.
succedentSame as conclusion.
syncategorematically Semantic construction: treatment of certain words (like negation and conjunction) in the construction rules instead of the lexicon.
syntactic structureHierachical structure specifying how the syntactic items making up a sentence relate to each other.
tableaux proofA tableaux refutation of AF is called a tableaux proof for A. It refutes the possibility of finding a model where A evaluates to F. Thus A must evaluate to T in all models, which is the definition of validity.
tableaux refutationA closed tableaux with the signed formula Aα at its root is called a tableaux refutation of Aα.
termFOL: Any constant or any variable is a term. Roughly speaking, terms are the noun phrases of first-order languages.
test calculusCalculi in which a proof is constructed by showing that the negation of the conjecture is unsatisfiable.
theoremA formula that is provable without any further assumptions is called a theorem.
true in a modelA sentence is true in a model iff for any assignment of variables in that model, the sentence is evaluated as being true by the interpretation function given in the model.
universalWe also call the 𝒯()F-rule universal rule.
validSee valid argument, valid formula, or valid sentence.
valid argumentAn argument is valid iff whenever all its premises are satisfied in some model using some variable assignment, then its conclusion is also satisfied in the same model using the same variable assignment.
valid formula A valid formula is a formula that is satisfied in all models (of the appropriate vocabulary) given any variable assignment.
validityProperty of being a valid formula.
valid sentenceA valid sentence is a sentence that is true in all models (of the appropriate vocabulary). Variable assignments need not be considered since sentences mustn't contain free variables.
variantLet g be an assignment of values to variables in some model, and let x be a variable. If g is an assignment of values to variables in the same model, and for all variables y such that y=x, g(y)=g(y) then we say that g is an (x-)variant of g.
vocabularyFOL: A vocabulary is an ordered pair of two sets. It enters into the specification of a first-order language by fixing what symbols will be used besides the logical symbols and variables to form expressions. The first set in a vocabulary contains the constant symbols to be used, the second set contains the symbols available for signifying properties and relations, each one paired with a number specifying its arity.
well-formed formulaFOL: formulae that are built from a vocabulary, the logical symbols of FOL and first-order variables according to the syntax rules of FOL.
well-typedIn typed λ-calculus, applications are only allowed if the type of the argument (to the right of the @ in the expression) is the same as the argument type of the functor (to the left of the @). The result of β-reducing such an application is then always of the result type of the functor. If all applications in an expression are allowed according to this criterion, the expression is well-typed.
witnessSame as skolem constant.
world knowledgeAll kinds of non-linguistic background knowledge (about the world) necessary for language processing. For our purposes think of world knowledge as a collection of formulae stating facts about the world. Typically, there will be basic facts like SIAMESECAT(MUTZ) and rule-like facts like x.SIAMESECAT(X)y.OWN(Y,X).
x-variantA variant of an assignment that changes the value assigned to x.
α-conversion The operation of producing an alphabetical variant of a λ-abstraction by replacing all occurences of the variable abstracted over by another one. Used (for instance) in λ-based semantic construction to avoid accidental variable bindings in the target representation.
α-equivalent Two λ-expressions are said to be α-equivalent if they can be transformed into each other by means of α-conversion.
β-reduction The process of substituting the argument of an application for the variable bound by the outmost λ in the functor (and dropping the outmost λ-prefix.
η-equivalent For functional expressions, it is always possible to abstract over any of the arguments, thereby making the functional character explicit. A functional expression is η-equivalent to any λ-expression resulting from abstraction over one or more of its arguments.
λ-abstraction A λ-abstraction can be formed from any well-formed lambda-expression (i.e. a first-order formula, an application or another abstraction) by prefixing a λ followed by a variable.
λ-boundThe variable occuring to the right of a λ-operator is λ-bound by this operator within the expression in its scope. If the same variable occurs to the right of another λ within that expression, it is in turn bound by this λ within its scope.
As an example, look at the following two λ-terms. The occurences of x are bound by the different λs as indicated by the colouring:
λ-structure A λ-expression written as a tree with variable-bindings indicated by so called binding edges.
∀∃-constellationAn existential quantification occuring within the scope of a universal quantifier. Such constellation may lead to infinite chains of rule-applications in automatic theorem proving and model generation.