Skip to content

an xtext based parser for the tptp grammer. (can be used to generate a java parser, and may lead to an awesome eclipse plugin)

License

Notifications You must be signed in to change notification settings

calypsomatic/tptpParser

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

8 Commits
 
 
 
 
 
 

Repository files navigation

tptpParser

An xtext based parser for the tptp grammer (http://www.cs.miami.edu/~tptp). (can be used to generate a java parser, and may lead to an awesome eclipse plugin)

this is built with xtext v2.4.3, and I welcom all patches and pull requests!

If you use this libray, I'd love to hear about it!

The design principles are:

  • the primary goal is the generated java parser, the eclipse plugin (while realy cool) is secondary
  • minimal/restrictive AST, we will ignore issues that happen in the extended biased problems, keeping is simple and restrictive will make it easier to use in compitition programs
  • grammar should be restrictive, no need for multiple lanuages in the same file
  • validate against all sample problems, this should be compititiion ready software
  • keep the eventual java parser and the eventual eclipse plugin (and the target tptp problem set in sync with version numbers)

global TODOs:

currently unsuported:

  • CNF
  • CL003-0.ax unclear "axiom" function above the or
  • that cnf problem
  • THF
  • CSR005^0.ax when did "@" become unirary, what does it even mean?
  • ...

About

an xtext based parser for the tptp grammer. (can be used to generate a java parser, and may lead to an awesome eclipse plugin)

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published