OpenQED Library Overview

This is an overview of the the OpenQED class library (scroll down for diagrams and descriptions of core classes).


Core Structure Classes (diagrams and descriptions below)
org.openqed.struct.formula Core structure classes for representing first order formulae (both CNF and FOF).
org.openqed.struct.misc Miscellaneous structure classes augmenting core structure classes.
org.openqed.struct.namedid Core structure classes for naming formula components (both static enumerations and dynamic names).
org.openqed.struct.sentence Core structure classes for representing sentences (annotated formulae, in TPTP nomenclature).


Parser Classes
org.openqed.parser.tptp Classes for parsing TPTP problems and generating core representational structures.


Command Line Tools
org.openqed.tool.clausifier Command line tool for converting FOF formulae to CNF formulae, optionally adding equality axioms.
org.openqed.tool.prover Command line tool for invoking very simple resolution based theorem prover (mainly place holder for future work).
org.openqed.tool.recognizer Command line tool for recognizing (parsing and validating) formula syntax and semantics.
org.openqed.tool.summarizer Command line tool for parsing formulae and generating structural summaries.
org.openqed.tool.treeprinter Command line tool for parsing and printing formulae in various formats.


Utility Classes
org.openqed.util Various utility classes.
org.openqed.util.prefs Classes for defining, parsing, checking, and generating help info for command line preferences.
org.openqed.util.tuple Classes representing generically-typed n-ary tuples.


This is an overview of the the OpenQED class library (scroll down for diagrams and descriptions of core classes).

At present, the functionality of this library is mostly limited to parsing, structuring, and manipulating problems in first order logic. The design of this library is heavily influenced by the TPTP problem library.

The core classes used for representing the structure of formulae are contained in three packages: org.openqed.struct.namedid, org.openqed.struct.formula, and org.openqed.struct.sentence. These packages build on each other in that order. That is, Sentences build upon Formulas, and both Sentences and Formulas build upon NamedIds.

Each of these three packages is described in a separate section below. Each description contains a class inheritance and composition diagram for the classes in the package. To aid in the interpretation of these diagrams, the very first section below gives a diagram key. And the very last section contains notes on various design decisions.


Diagram Key

Here is a key to help with interpreting the below diagrams (description follows):

Interface names are given in magenta, abstract base class names are given in blue, and concrete instantiable class names are given in black. The return type, name, and arguments of important methods are listed below the interface or class name on which they are defined. Only the most illustrative methods of each class are shown. If a class implements an interface, that will be indicated on the line immediately below the class name. Some classes have a fixed set of static instances. These enumeration classes list their instances in red ALL_CAPS. In some cases this list is abbreviated. Inheritance relationships between super and sub classes are shown using solid black lines. Compositional relationships between classes are shown using dashed gray arrows, with a single arrowhead indicating a 1:1 relationship, and a double arrowhead indicating a 1:N relationship.

The class names in the diagrams below are clickable and are linked to their corresponding JavaDoc documentation (which at the moment is quite lacking). If the diagrams below are too wide for your screen, you might try viewing this page with no frames.

NamedId Package Overview

The following diagram shows the primary structure of the classes in the org.openqed.struct.namedid package (description follows):

NamedIds represent textual string-valued names of various formula and sentence components. NamedIds are either DynamicIds or EnumIds. DynamicIds are dynamically defined by the user at runtime with a string value that can be anything within the limits prescribed by the particular DynamicId concrete sub class. FunctorIds are DynamicIds which are defined with an additional user specified arity. EnumIds are statically defined as one of a fixed set of instance values prescribed by the particular EnumId concrete sub class. InvertibleEnumIds are EnumIds which have complementary inverse values.

NamedIds are constructed using interning such that there will never be two distinct instances N1 and N2 such that N1.equals(N2). That is, N1.equals(N2) is always equivalent to N1==N2.

DynamicIds belong to and are unique within a DynamicIdSpace (not yet documented). Every SentenceList (which is a list of annotated formulae, and is described below) has its own DynamicIdSpace. Within a DynamicIdSpace, it is possible to temporarily construct anonymous DynamicIds, which still allow for identity and equality testing, but which have not yet been assigned a textual string-valued name. Anonymous SentenceIds are useful when creating equality or other theory axioms, and anonymous FunctionIds and VariableIds are useful when creating Skolem functions and standard variables. Before the SentenceList is printed or output to a file, anonymous DynamicIds can be systematically assigned names unique within the DynamicIdSpace.

NamedIds are immutable.

Formula Package Overview

The following diagram shows the primary structure of the classes in the org.openqed.struct.formula package (description follows):

First order formulae (both CNF and FOF) are represented as tree structures whose nodes are instances of FormulaNode sub classes. That is, FormulaNodes are tree nodes with other FormulaNodes as children. The upper portions of such trees are composed of nodes of class Formula, and the lower portions of such trees are composed of nodes of class Term. The number and class of children that a particular sub class of FormulaNode is allowed to have is indicated by the dashed gray arrows in the above diagram.

Sentences (described in the next section) are not part of the formula package. The Sentence class is added to the above diagram to show the compositional relationship between Sentences and RootFormulas.

RootFormulas are either CnfFormulas or FofFormulas. CnfFormulas are composed of one or more Literals, each of which is composed of a UnaryOperator (either NEGATION or IDENTITY) and a single AtomicFormula child. AtomicFormulas can be either NullaryFormulas (having a NullaryOperator value of either CONTRADICTION or TAUTOLOGY) or PredicateFormulas which have a PredicateId and zero or more Term children.

FofFormulas are either AtomicFormulas (having no FofFormula children), BinaryFormulas (having two FofFormula children), NegationFormulas, or QuantifierFormulas (the latter two having only one FofFormula child).

Terms are either FunctionTerms, ObjectTerms, or VariableTerms. FunctionTerms have a FunctionId and zero or more Term children. ObjectTerms represent distinct constants in TPTP nomenclature.

Because of the limitations of Java inheritance, the common characteristic of having a FunctorId and Term children, shared between FunctionTerms and PredicateFormulas, is implemented by the FunctorApplication interface. For similar reasons, Literals and NegationFormulas both implement the UnaryFormula interface (although NegationFormulas are constrained to having only NEGATION as their UnaryOperator). Note that the return types of FunctorApplication.getFunctorId() and UnaryFormula.getSubFormula() are narrowed appropriately by their implementing classes.

FormulaNode trees are immutable.

Sentence Package Overview

The following diagram shows the primary structure of the classes in the org.openqed.struct.sentence package (description follows):

Sentences represent annotated formulae in TPTP nomenclature. A first order logic problem or solution is represented as a SentenceList. TODO: more...

SentenceLists, Sentences, and SentenceSources are immutable.

Design notes

TODO: Discuss: