A |

application in ontology reasoning | Progress in Automating Higher-Order Ontology Reasoning |

automated reasoning | Automated Reasoning in the Simulation of Evolvable Systems Automated Higher-order Reasoning about Quantales |

B |

Benchmarking | GridTPT: a distributed platform for Theorem Prover Testing A Comparison of Solvers for Propositional Dynamic Logic |

Boolean extensionality and modalities | Progress in Automating Higher-Order Ontology Reasoning |

C |

component systems | Automated Reasoning in the Simulation of Evolvable Systems |

connection calculus | Using the TPTP Language for Representing Derivations in Tableau and
Connection Calculi |

D |

decision procedures | Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus A Comparison of Solvers for Propositional Dynamic Logic |

Development support | GridTPT: a distributed platform for Theorem Prover Testing |

Dummett Logic | Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus |

E |

Evolvable systems | Automated Reasoning in the Simulation of Evolvable Systems |

G |

geometry | Automation for Geometry in Isabelle/HOL |

Grid Computing | GridTPT: a distributed platform for Theorem Prover Testing |

H |

higher-order reasoning | Automated Higher-order Reasoning about Quantales |

higher-order theorem proving | Progress in Automating Higher-Order Ontology Reasoning |

I |

Isabelle | Automation for Geometry in Isabelle/HOL |

P |

Performance aspects | GridTPT: a distributed platform for Theorem Prover Testing |

prime implicates | Trie Based Subsumption and Improving the pi-Trie Algorithm |

propositional dynamic logic | A Comparison of Solvers for Propositional Dynamic Logic |

Q |

QEPCAD | Automation for Geometry in Isabelle/HOL |

quantale | Automated Higher-order Reasoning about Quantales |

S |

simplification | Automation for Geometry in Isabelle/HOL |

subsumption | Trie Based Subsumption and Improving the pi-Trie Algorithm |

T |

tableau calculus | Using the TPTP Language for Representing Derivations in Tableau and
Connection Calculi |

tableaux | Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus |

test | GridTPT: a distributed platform for Theorem Prover Testing |

TPTP language | Using the TPTP Language for Representing Derivations in Tableau and
Connection Calculi |

Tries | Trie Based Subsumption and Improving the pi-Trie Algorithm |

typed higher-order form of TPTP | Automated Higher-order Reasoning about Quantales |