Code Index View Download

-conversion. View Download

Driver, combine-rules, semantic Macros. View Download

Working with USRs, tree predicates, translation of solved forms into -terms. View Download

Auxiliaries. View Download

Operator definitions. View Download

Grammar rules for discourse. View Download

The translation from DRT to predicate logic. View Download

The drivers for DRS construction and the semantic macros. View Download

The DCG-rules and the lexicon (using module ). From here, the combine-rules and lexical macros are called. View Download

The lexical entries for a small fragment of English. View Download

Some example models to play with. View Download

The code for our first attempt at semantic construction, using the +-operator and insertArgs/2. View Download

DCG for semantic construction using -calculus. View Download

The drivers for model generation and theorem proving. View Download

The tableaux itself: tabl/6 View Download

The driver predicate; definition of the combine-rules and the lexical macros for -calculus. View Download

The driver predicate evaluate/2 and the core clauses of the model checker (eval/2). View Download

The wrapper for model generation and theorem proving: modGen/3 and theorem/1. View Download

The core of the implementation: tabl/3 and clash/3 View Download

Reading the input from stdin. View Download

The revised version of the model checker (excluding wff/1, which you have to provide yourself). View Download

Driver predicate for our first lambda approach. View Download

newconst/1 View Download

Solving: normalization and distribution. View Download

subst/3 View Download

Our very first experimental DCG.

Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)