PSL Downloads

The table below links to various portions of PSL in a number of formats (or download them all here). The number of parts of PSL included in each link increases down the rows, see the ontology page. Each link in the right three coloumns is to a single file in the corresponding format, suitable for loading into an automated theorem prover. Files in the CLIF column are in the Common Logic Interchange Format, using the question mark prefix convention for variable names. CLIF syntax was checked with parsers from Pando and the developers of Tau. Files in the MIV KIF column are in a variant of CLIF for use with Minimal Interface to Vampire. It is the same as CLIF, except uses “=>” for “if”, “ <=> ” for “iff”, and “equal” for “=”. Files in the Tau KIF column are a variant of CLIF for use with the Tau theorem prover. They have the same differences from CLIF as MIV KIF, except retain “=” for equality. The “d” files embed HTML from these pages as comments.

Download all the above files here. The ontology pages are contained in this psl-ontology.zip file, not including server scripts ( non-governmental external links can be extracted from the server link).