A |

ATP Competitions | Machine Learner for Automated Reasoning 0.4 and 0.5 |

automated reasoning | Machine Learner for Automated Reasoning 0.4 and 0.5 |

automated theorem proving | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics Beagle as a HOL4 external ATP method Automated Theorem Proving using the TPTP Process Instruction Language |

automated theorem proving process | Automated Theorem Proving using the TPTP Process Instruction Language |

B |

Beagle | Beagle as a HOL4 external ATP method |

C |

constraints | A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses |

D |

de Bruijn | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation |

Description Logics | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics |

discrimination tree | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation |

E |

EPR | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics |

equational logic | A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses |

F |

first-order logic | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics |

formal mathematics | Machine Learner for Automated Reasoning 0.4 and 0.5 |

G |

geometric logic | Razor: Provenance and Exploration in Model-Finding |

H |

HOL4 | Beagle as a HOL4 external ATP method |

I |

instance-based theorem proving | SGGS Theorem Proving: an Exposition |

L |

large theories | Machine Learner for Automated Reasoning 0.4 and 0.5 |

M |

machine learning | Machine Learner for Automated Reasoning 0.4 and 0.5 |

model finding | A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories Razor: Provenance and Exploration in Model-Finding |

model-based theorem proving | SGGS Theorem Proving: an Exposition |

P |

polymorphism | Polymorphic+Typeclass Superposition |

prime implicates | A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses |

Provenance | Razor: Provenance and Exploration in Model-Finding |

Q |

Quantifier Instantiation | A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories |

S |

semantic guidance | SGGS Theorem Proving: an Exposition |

substitution | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation |

superposition | Polymorphic+Typeclass Superposition |

superposition calculus | A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories |

T |

term representation | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation |

theorem proving | Polymorphic+Typeclass Superposition |

TPTP | Automated Theorem Proving using the TPTP Process Instruction Language |

TPTP Process Instruction language | Automated Theorem Proving using the TPTP Process Instruction Language |

U |

unification | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation |