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 |