Glossary

abstracted over	When 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 pronoun	Anaphoric 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 formula	Atomic formulae are formulae that do not contain any connectives.
axiom	Formulas 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 edge	Additional 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 rule	Tableaux 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 function	Function 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 Rule	CLLS: Rule that allows for two alternative resolutions of certain CLLS-dominance constraints. (Same as ^↗Distribution Rule)
closed	A tableaux is closed iff it contains at least one pair of contradictory literals on each of its branches.
combinatorial explosion	Combinatorial 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.
complete	A 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 tree	A 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 symbol	First 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-free	Model-generation: A set of literals is contradiction-free if it doesn't contain literals AT and AF at the same time.
conversational implicature	Intentions 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 maxim	Specific maxims subsidiary to the general ^↗cooperative principle assumed to be followed by participants in a conversation.
cooperative principle	Principle 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 storage	Cooper 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.
correct	A 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-compositionality	Compositionality 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 procedure	A 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 theorem	Theorem relating logical consequence and the object language conditional. E.g. the deduction theorem for propositional logic is: P→Q,P⊧Q
derivability	Calculi: 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 rule	Rules 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.
discourse	A 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 referent	Discourse 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.
disjunctive	Tableaux calculi: An expansion by which at least one new branch is added to a tableaux is called a disjunctive expansion.
Distribution Rule	Rule 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 edge	CLLS: Dominance edges are edges indicating underspecified scoping in constraint graphs. Usually drawn as dotted lines.
donkey sentence	Sentences 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 model	A model is an exact model for a given language if for each entity in its domain, there is exactly one constant in the language.
existential	The rule for the existential quantifier in tableaux calculi is also called the ^↗existential rule.
fairness	A tableaux expansion algorithm is called fair if every multiply expandible formula gets expanded equally often in the limit.
finite model property	A 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 formula	Syntactic entitities of first order logic that are assigned truth-values in a given model.
first-order language	Set 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 model	A 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 variable	Variables (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 application	The concatenation of a λ-prefixed expression with its argument (additionally marked by an @-symbol in our notation)
Herbrand base	The set of all constant symbols of a language.
Herbrand model	A model for a language that has as its domain the ^↗Herbrand base of that language.
inference	FOL: 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 system	A ^↗calculus.
initial tableaux	Tableaux calculi: A tableaux containing only a (negated) conjecture and possibly (positive) world knowledge.
instance	Calculi: The result of substituting actual formulas for schematic letters in Axiom schemata.
interpretation	The 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 function	Second 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-deepening	Generally: 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 storage	A revision of ^↗Cooper storage that solves some obvious problems with the original approach. (Same as ^↗Nested Cooper storage)
lexical semantic	Field of research that studies relations between and structures of meanings of single words.
lingua universalis	Language that Leibniz envisaged to be used by people to formulate their problems so that they become automatically decidable, following his motto "Calculemus!" .
literal	Atomic formulae and negated atomic formulae
logical constant	A 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).
manner	One of the ^↗conversational maxims assumed by Grice. It is stated as follows: Be relevant.
matrix	Formula from which a quantification is formed.
meaning construction	Given 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 model	Some 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 generation	Inference process that derives from a formula a set of literals specifying a model for that formula.
model generation procedure	Algorithm for model generation.
modus ponens	Inference pattern by which, given a conditional and its antecedent, the consequent is derived.
name	FOL: same as constant symbols.
negative	Calculi: Negative calculi are ^↗test calculus.
negative calculus	Calculus in which a proof is constructed by showing that the negation of the conjecture is unsatisfiable.
Nested Cooper storage	Same as ^↗Keller storage.
normal dominance constraint	Formal language used for giving underspecified descriptions of λ-expressions. Equivalent linear notation for ^↗constraint graphs.
normalization	CLLS: Deterministic steps in the process of solving dominance constraints.
normal model	A 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).
open	A 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 normalization	CLLS: 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 symbol	FOL: 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.
pronoun	Pronouns 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.
proof	Sequence 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 theory	Proof 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.
provability	Property of being ^↗provable.
provable	A 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.
quality	One of the ^↗conversational maxims assumed by Grice. It is stated as follows: Try to make your contribution one that is true.
quantifier store	Structure used by the semantic construction technique of ^↗Cooper storage to store semantic representations of NPs for later application.
quantifying in	Montague'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.
quantity	One of the ^↗conversational maxims assumed by Grice. It is stated as follows: Make your contribution as informative as is required.
redundancy elimination	Normalization 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 proof	A proof that procedes by refuting the negation of the original conjecture, i.e. by showing that this negation is unsatisfiable.
relation	One of the ^↗conversational maxims assumed by Grice. It is stated as follows: Be perspicuous
relation symbol	FOL: Syntactic entities used to formalize words for properties and relations.
result type	Type of the result of a functional application. Needs to be specified when constructing the respective functional type.
satisfiability	CLLS: A dominance constraint is satisfiable if there is at least one λ-structure into which it can be embedded.
saturated	A tableaux is said to be saturated if no rule can be applied to any of the formulae on it producing a new result.
s-compositionality	Compositionality 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.
scope	Formula to which a universal quantifier and a quantified variable are prefixed when forming a quantification. Same as ^↗matrix.
scope ambiguity	Semantic 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-decidable	A 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.
sentence	FOL: A first-order formula without any free variables.
signature	FOL: same as ^↗vocabulary.
signed	Calculi: 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 formulae	See ^↗signed.
simply typed λ-calculus	Version of λ-calculus where types pre-specifying reducible applications enter into the wellformedness conditions.
skolem constant	A new constant symbol that is introduced when expanding an existential quantification.
solution	CLLS: A λ-structure is a solution of a constraint graph if the constraint graph ^↗describe that λ-structure.
solved form	CLLS: 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
sound	Calculi: Same as ^↗correct.
specification	Listing 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.
subformula	FOL: part of a formula that is itself a formula according to the syntax of FOL.
subordination	Structural notion in DRT capturing the accessibility of discourse referents for anaphoric reference in terms of nesting of DRSs.
succedent	Same as ^↗conclusion.
syncategorematically	Semantic construction: treatment of certain words (like negation and conjunction) in the construction rules instead of the lexicon.
syntactic structure	Hierachical structure specifying how the syntactic items making up a sentence relate to each other.
tableaux proof	A 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 refutation	A closed tableaux with the signed formula Aα at its root is called a tableaux refutation of Aα.
term	FOL: Any constant or any variable is a term. Roughly speaking, terms are the noun phrases of first-order languages.
test calculus	Calculi in which a proof is constructed by showing that the negation of the conjecture is unsatisfiable.
theorem	A formula that is provable without any further assumptions is called a theorem.
true in a model	A 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.
universal	We also call the 𝒯(∃)F-rule universal rule.
valid	See ^↗valid argument, ^↗valid formula, or ^↗valid sentence.
valid argument	An 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.
validity	Property of being a ^↗valid formula.
valid sentence	A 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.
variant	Let 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.
vocabulary	FOL: 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 formula	FOL: formulae that are built from a vocabulary, the logical symbols of FOL and first-order variables according to the syntax rules of FOL.
well-typed	In 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.
witness	Same as ^↗skolem constant.
world knowledge	All 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-variant	A ^↗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.
λ-bound	The 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: λx.Woman(x)λx.Woman(x)∨λx.Man(x)(x)
λ-structure	A λ-expression written as a tree with variable-bindings indicated by so called ^↗binding edges.
∀∃-constellation	An 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.