Package com.articulate.sigma.trans

Class THF

java.lang.Object

com.articulate.sigma.trans.THF

public class THF
extends Object

This class handles the conversion of problems (= axioms + queries) from their KIF representation into a THF representation; THF is the TPTP standard for classical higher-order logic, i.e. Church's simple theory. The main function provided is KIF2THF(KIFaxioms,KIFqueries,KnowledgeBase) A challenge part in this transformation is the computation of an appropriate typing for the KIF terms and formulas. This is partly non-trivial. The conversion is intended to work purely syntactically (when no typing-relevant information from SUMO is available) or mixed syntactically-semantically (when typing-relevant information from SUMO is available). A small example: The KIF Problem with axioms (holdsDuring (YearFN n2009) (enjoys Mary Cooking)) (holdsDuring (YearFN n2009) (=> (instance ?X Female) (wants Ben ?X))) (holdsDuring ?X (instance Mary Female)) and Query (holdsDuring ?X (and (?Y Mary Cooking) (wants ?Z Mary))) is translated into the THF problem: %%% The extracted Signature %%% thf(holdsDuring,type,(holdsDuring: ($i>$o>$o))). thf(enjoys_THFTYPE_IiioI,type,(enjoys_THFTYPE_IiioI: ($i>$i>$o))). thf(female,type,(female: $i)). thf(n2009,type,(n2009: $i)). thf(cooking,type,(cooking: $i)). thf(ben,type,(ben: $i)). thf(yearFN_THFTYPE_IiiI,type,(yearFN_THFTYPE_IiiI: ($i>$i))). thf(mary,type,(mary: $i)). thf(wants,type,(wants: ($i>$i>$o))). thf(instance_THFTYPE_IiioI,type,(instance_THFTYPE_IiioI: ($i>$i>$o))). %%% The translated axioms %%% thf(ax,axiom,((! [X: $i]: (holdsDuring @ X @ (instance_THFTYPE_IiioI @ mary @ female))))). thf(ax,axiom,((! [X: $i]: (holdsDuring @ (yearFN_THFTYPE_IiiI @ n2009) @ ((instance_THFTYPE_IiioI @ X @ female) => (wants @ ben @ X)))))). thf(ax,axiom,((holdsDuring @ (yearFN_THFTYPE_IiiI @ n2009) @ (enjoys_THFTYPE_IiioI @ mary @ cooking)))). %%% The translated conjectures %%% thf(con,conjecture,((? [X: $i,Y: $i,Z: $i]: (holdsDuring @ X @ ((enjoys_THFTYPE_IiioI @ mary @ Y) invalid input: '&' (wants @ Z @ mary)))))). This THF problem can be solved effectively by TPTP THF compliant higher-order theorem provers. The transformation often needs to introduce several 'copies' of KIF constants for different THF types. Therefore, some constant symbols become tagged with type information during the transformation process. Example for tagged constant symbols above enjoys_THFTYPE_IiioI and instance_THFTYPE_IiioI.

Author:

Christoph Benzmueller c.benzmueller [at] fu-berlin [dot] de

Constructor Summary

Constructors

Constructor	Description
THF()	reset the axiom counters

Method Summary

Modifier and Type	Method	Description
List<String>	KIF2THF(Collection<Formula> axiomsC, Collection<Formula> conjecturesC, KB kb)	The main function to convert KIF problems into TPTP THF representation; see the explanation at top of this file.
static void	main(String[] args)	A test method.
String	oneKIF2THF(Formula form, boolean conjecture, KB kb)
static void	showHelp()
static void	test(KB kb)
static List<String>	transModalTHF(KB kb)
static List<String>	transTHF(KB kb)
static void	writeTHF(KB kb, List<String> kbAll2)

Methods inherited from class java.lang.Object

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

Constructor Details

THF

public THF()

reset the axiom counters

Method Details

oneKIF2THF

public String oneKIF2THF(Formula form,
 boolean conjecture,
 KB kb)

KIF2THF

public List<String> KIF2THF(Collection<Formula> axiomsC,
 Collection<Formula> conjecturesC,
 KB kb)

The main function to convert KIF problems into TPTP THF representation; see the explanation at top of this file. This is the only public function of THF.java so far.

Parameters:

axiomsC - is a list of KIF axiom formulas

conjecturesC - is a list of KIF query formulas

kb - is a knowledge base, e.g. SUMO

transModalTHF

public static List<String> transModalTHF(KB kb)

transTHF

public static List<String> transTHF(KB kb)

writeTHF

public static void writeTHF(KB kb,
 List<String> kbAll2)

test

public static void test(KB kb)

showHelp

public static void showHelp()

main

public static void main(String[] args)

A test method.