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 |