| 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 |
