Download

• The Sibyl prover (Linux binaries).
  
  
• Sibyl User Guide
  
  
• HLtranslate (Linux binaries): a tool implementing the standard translation of hybrid logic and assertions into first order logic. The result is a file in the syntax of the Spass prover.

  It can also be used to convert files from Sibyl syntax to HTab syntax, provided that they do not contain converse modalities (that are not allowed by HTab).

  Its use and the available options are shown when calling the tool (from the command line) with the option -help