abstracted over | When forming an abstraction, the variable in the |

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 that refer back to textual antecedents.^{↗}pronoun |

antecedent | Calculi: The antecedents (also called ) 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. ^{↗}premises |

argument type | A version of |

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 tree notation for ^{↗} |

bound variable | A quantifier is said to bind the variable standing immediately to its right. Within a quantification of the form |

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 () and then finding out who is right by mechanically applying a simple system of formal rules (^{↗}lingua universalis).^{↗}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 and ^{↗}proofderivation. If a calculus is and ^{↗}sound with respect to the semantics of a logic, it can be used to prove the (semantic) validity of formulae in that logic. ^{↗}complete |

calculus ratiocinator | The set of rules to be used by the disputants in Leibniz' -scenario to settle their differences by purely formal calculation. ^{↗}calculemus |

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 |

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 |

contradiction-free | Model-generation: A set of literals is contradiction-free if it doesn't contain literals |

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 assumed to be followed by participants in a conversation.^{↗}cooperative principle |

cooperative principle | Principle characterising conversation as a rational cooperative activity. According to H.P. Grice this principle, and more specifically the 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. ^{↗}conversational maxims |

Cooper storage | Cooper storage is an early approach to dealing with quantifier scope ambiguities in with semantic representations. ^{↗}quantifier stores |

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: |

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 |

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 , above the conditions on them.^{↗}DRS |

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 |

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 rule.^{↗}existential |

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 ) and a function (the ^{↗}domain) 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.^{↗}interpretation function |

first order tableaux | |

free variable | Variables (in well formed expressions) that are not . For an explicit formal definition of the concepts of ^{↗}bound and ^{↗}bound, see the main text.^{↗}free variable |

functional application | The concatenation of a |

Herbrand base | The set of all constant symbols of a language. |

Herbrand model | A model for a language that has as its domain the of that language.^{↗}Herbrand base |

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 |

interpretation function | Second element of a . A function assigning an element from the domain to each non-variable, non-logical symbol of the language under consideration.^{↗}first-order model |

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 that solves some obvious problems with the original approach. (Same as ^{↗}Cooper storage)^{↗}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 assumed by Grice. It is stated as follows: ^{↗}conversational maximsBe 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 . When talking about model generation in this course, we take sets of literals as a scientific simplification of mental models.^{↗}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 .^{↗}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. |

open | A branch of a tableaux is called iff it contains no contradictory literals. Alternatively, one can have a rule that derives a special symbol (such as ^{↗}open |

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 ) 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. ^{↗}antecedents |

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 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.^{↗}calculus |

proof from the assumptions in ℋ | Proof that may contain formulas from a set .^{↗}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 |

quality | One of the assumed by Grice. It is stated as follows: ^{↗}conversational maximsTry to make your contribution one that is true. |

quantifier store | Structure used by the semantic construction technique of to store semantic representations of NPs for later application. ^{↗}Cooper storage |

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 assumed by Grice. It is stated as follows: ^{↗}conversational maximsMake 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 assumed by Grice. It is stated as follows: ^{↗}conversational maximsBe 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 |

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 signed themselves. |

signed formulae | See .^{↗}signed |

simply typed λ-calculus | Version of |

skolem constant | A new constant symbol that is introduced when expanding an existential quantification. |

solution | CLLS: A that ^{↗}describe |

solved form | CLLS: A constraint graph is in solved form if it has no cycles that use only solid and , and none of its nodes has two incoming edges that are solid or dominance^{↗}dominance edges |

sound | Calculi: Same as .^{↗}correct |

specification | Listing of literals used to represent a . It contains all literals that are true in the model, all others are assumed to be false.^{↗}Herbrand model |

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 .^{↗}validity |

tableaux refutation | A closed tableaux with the signed formula |

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 |

valid | See , ^{↗}valid argument, or ^{↗}valid formula.^{↗}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 |

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 |

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 |

x-variant | A of an assignment that changes the value assigned to x.^{↗}variant |

α-conversion | The operation of producing an alphabetical variant of a |

α-equivalent | Two |

β-reduction | The process of substituting the argument of an application for the variable bound by the outmost |

η-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 |

λ-abstraction | A |

λ-bound | The variable occuring to the right of a its scope.As an example, look at the following two |

λ-structure | A . ^{↗}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. |