A |

automated reasoning | Improving Statistical Linguistic Algorithms for Parsing Mathematics |

automated theorem proving | Implementing Polymorphism in Zenon Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry |

B |

backtracking | Functional Pearl: the Proof Search Monad |

Boolean calculus | A Method to Simplify Expressions: Intuition and Preliminary Experimental Results |

C |

coinduction | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial |

Coinductive predicate | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial |

Compression | Clausal Proof Compression |

computational linguistics | Improving Statistical Linguistic Algorithms for Parsing Mathematics |

D |

Dedukti | Defining the meaning of TPTP formatted proofs |

derivation | Functional Pearl: the Proof Search Monad |

E |

equivalence problem | A Method to Simplify Expressions: Intuition and Preliminary Experimental Results |

F |

first-order logic | Implementing Polymorphism in Zenon |

Flyspeck | Improving Statistical Linguistic Algorithms for Parsing Mathematics |

G |

glucose | On Reducing Clause DataBase in Glucose |

greatest fixpoint | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial |

H |

higher-order logic | Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving |

HOL Light | Improving Statistical Linguistic Algorithms for Parsing Mathematics |

I |

induction | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial |

inductive predicate | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial |

interpretation | The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps |

L |

large-theory automated reasoning | Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry |

learnt clause database | On Reducing Clause DataBase in Glucose |

least fixpoint | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial |

Logistic Supply Chain | Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving |

M |

mechanical proof assistant | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial |

ML Polymorphism | Implementing Polymorphism in Zenon |

model | The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps |

monad | Functional Pearl: the Proof Search Monad |

N |

nbSAT | On Reducing Clause DataBase in Glucose |

P |

Parsing Mathematics | Improving Statistical Linguistic Algorithms for Parsing Mathematics |

probability theory | Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving |

proof | Clausal Proof Compression |

proof certification | Defining the meaning of TPTP formatted proofs |

proof search | Functional Pearl: the Proof Search Monad |

proofcert | Defining the meaning of TPTP formatted proofs |

R |

Reliability Block Diagrams | Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving |

Representation of sets of equivalent terms | A Method to Simplify Expressions: Intuition and Preliminary Experimental Results |

S |

SAT | Clausal Proof Compression |

Simplification of expressions | A Method to Simplify Expressions: Intuition and Preliminary Experimental Results |

T |

tableau method | Implementing Polymorphism in Zenon |

Tarskian Geometry | Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry |

TPTP | Defining the meaning of TPTP formatted proofs The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps |

TSTP | Defining the meaning of TPTP formatted proofs |

type checking | Improving Statistical Linguistic Algorithms for Parsing Mathematics |

V |

verification | Functional Pearl: the Proof Search Monad |