Software

• Sibyl, a tableau based prover for hybrid logic with binders, converse and global modalities, transitive relations and relation hierarchies.
  
  
• Pilate and Herod, two tableau provers for basic hybrid logic.
  
  
• Logitest, a support system for logical MCQs designers.
  
  
• The Planner Pdk, a planner based on the encoding of planning problems into Linear Temporal Logic.