org.qedeq.kernel.se.base.module
Interface InitialPredicateDefinition

All Superinterfaces:

NodeType

All Known Implementing Classes:

InitialPredicateDefinitionVo

public interface InitialPredicateDefinition
extends NodeType

Initial Definition of operator. This is a basic predicate constant. For example: "x is element of y".

Author:

Michael Meyling

Method Summary

java.lang.String	getArgumentNumber() Get number of arguments for the defined object.
LatexList	getDescription() Get description.
java.lang.String	getLatexPattern() Get LaTeX output for definition.
java.lang.String	getName() This name together with getArgumentNumber() identifies a predicate.
Element	getPredCon() Get new predicate constant with free subject variables.

Methods inherited from interface org.qedeq.kernel.se.base.module.NodeType

getAxiom, getFunctionDefinition, getInitialFunctionDefinition, getInitialPredicateDefinition, getPredicateDefinition, getProposition, getRule

Method Detail

getArgumentNumber

java.lang.String getArgumentNumber()

Get number of arguments for the defined object. Carries information about the argument number the defined object needs.

Returns:

Argument number.

getName

java.lang.String getName()

This name together with getArgumentNumber() identifies a predicate.

Returns:

Name of defined predicate.

getLatexPattern

java.lang.String getLatexPattern()

Get LaTeX output for definition. The replaceable arguments must are marked as "#1", "#2" and so on. For example "\mathfrak{M}(#1)"

Returns:

LaTeX pattern for definition type setting.

getPredCon

Element getPredCon()

Get new predicate constant with free subject variables. The predicate constant must match getName() and getArgumentNumber().

Returns:

Predicate constant with free subject variables.

getDescription

LatexList getDescription()

Get description. Optional.

Returns:

Description. Might be null.