IWIL-2015:Keyword Index

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