Package com.articulate.sigma.trans

Class Modals

java.lang.Object

com.articulate.sigma.trans.Modals

public class Modals
extends Object

Field Summary

Fields

Modifier and Type	Field	Description
static final List<String>	allowedHeads
static final List<String>	dualFormulaPreds
static final List<String>	formulaPreds
static final Set<String>	MODAL_RELATIONS
static final Set<String>	modalAttributes
static final Set<String>	noWorld
static final List<String>	regHOL3pred
static final List<String>	regHOLpred
static final Set<String>	RESERVED_MODAL_SYMBOLS
static final Set<String>	RIGID_RELATIONS

Constructor Summary

Constructors

Constructor	Description
Modals()

Method Summary

Modifier and Type	Method	Description
static void	addAccrelnDef(KB kb)	Add the signature for the Kripke accessibility relation
static String	baseFunctor(String head)	Return the base functor name by stripping a trailing "__" suffix.
static void	doTQM10Tests(KB kb)	Tests based on ~/workspace/sumo/tests/TQM10.kif Uses same KB instance as main method
static String	getTFFHeader()
static String	getTHFHeader()
static Formula	handleHOL3pred(Formula f, KB kb, Integer worldNum)	Handle the predicates given in regHOL3pred, which have a parameter followed by a formula.
static Formula	handleHOLpred(Formula f, KB kb, Integer worldNum)	Handle predicates in regHOLpred that take an individual and a formula argument, e.g.
static Formula	handleModalAttribute(Formula f, KB kb, Integer worldNum)	Handle the predicate modalAttribute: (modalAttribute F M) is read as: "F holds in all worlds accessible via modality M".
static void	main(String[] args)
static Formula	processModals(Formula f, KB kb)
static Formula	processRecurse(Formula f, KB kb, Integer worldNum)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

formulaPreds

public static final List<String> formulaPreds

dualFormulaPreds

public static final List<String> dualFormulaPreds

regHOL3pred

public static final List<String> regHOL3pred

regHOLpred

public static final List<String> regHOLpred

modalAttributes

public static final Set<String> modalAttributes

RIGID_RELATIONS

public static final Set<String> RIGID_RELATIONS

MODAL_RELATIONS

public static final Set<String> MODAL_RELATIONS

RESERVED_MODAL_SYMBOLS

public static final Set<String> RESERVED_MODAL_SYMBOLS

allowedHeads

public static final List<String> allowedHeads

noWorld

public static final Set<String> noWorld

Constructor Details

Modals

public Modals()

Method Details

handleHOL3pred

public static Formula handleHOL3pred(Formula f,
 KB kb,
 Integer worldNum)

Handle the predicates given in regHOL3pred, which have a parameter followed by a formula.

handleHOLpred

public static Formula handleHOLpred(Formula f,
 KB kb,
 Integer worldNum)

Handle predicates in regHOLpred that take an individual and a formula argument, e.g. (confersObligation USGovernment ?A F). We rewrite them into a Kripke-style implication using accreln: (P A F) ==> (=> (accreln P A ?W_{n-1} ?W_n) F') where F' is recursively processed and world-indexed, and we introduce a fresh world variable ?Wn.

handleModalAttribute

public static Formula handleModalAttribute(Formula f,
 KB kb,
 Integer worldNum)

Handle the predicate modalAttribute: (modalAttribute F M) is read as: "F holds in all worlds accessible via modality M". We rewrite: (modalAttribute F M) into (=> (accrelnP M ?W_{n-1} ?W_n) F') where F' is recursively processed and world-indexed, and we introduce a fresh world variable ?Wn.

processRecurse

public static Formula processRecurse(Formula f,
 KB kb,
 Integer worldNum)

baseFunctor

public static String baseFunctor(String head)

Return the base functor name by stripping a trailing "__" suffix. E.g. "partition__7" -> "partition", "disjointDecomposition__4" -> "disjointDecomposition". If there is no such suffix, returns the input unchanged.

addAccrelnDef

public static void addAccrelnDef(KB kb)

Add the signature for the Kripke accessibility relation

processModals

public static Formula processModals(Formula f,
 KB kb)

getTFFHeader

public static String getTFFHeader()

getTHFHeader

public static String getTHFHeader()

doTQM10Tests

public static void doTQM10Tests(KB kb)

Tests based on ~/workspace/sumo/tests/TQM10.kif Uses same KB instance as main method

main

public static void main(String[] args)