IWIL-2015: Keyword Index

KeywordPapers
a
automated reasoningImproving Statistical Linguistic Algorithms for Parsing Mathematics
automated theorem provingImplementing Polymorphism in Zenon
Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry
b
backtrackingFunctional Pearl: the Proof Search Monad
Boolean calculusA Method to Simplify Expressions: Intuition and Preliminary Experimental Results
c
coinductionWell-founded Functions and Extreme Predicates in Dafny: A Tutorial
Coinductive predicateWell-founded Functions and Extreme Predicates in Dafny: A Tutorial
CompressionClausal Proof Compression
computational linguisticsImproving Statistical Linguistic Algorithms for Parsing Mathematics
d
DeduktiDefining the meaning of TPTP formatted proofs
derivationFunctional Pearl: the Proof Search Monad
e
equivalence problemA Method to Simplify Expressions: Intuition and Preliminary Experimental Results
f
first-order logicImplementing Polymorphism in Zenon
FlyspeckImproving Statistical Linguistic Algorithms for Parsing Mathematics
g
glucoseOn Reducing Clause DataBase in Glucose
greatest fixpointWell-founded Functions and Extreme Predicates in Dafny: A Tutorial
h
higher-order logicTowards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving
HOL LightImproving Statistical Linguistic Algorithms for Parsing Mathematics
i
inductionWell-founded Functions and Extreme Predicates in Dafny: A Tutorial
inductive predicateWell-founded Functions and Extreme Predicates in Dafny: A Tutorial
interpretationThe Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps
l
large-theory automated reasoningExperiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry
learnt clause databaseOn Reducing Clause DataBase in Glucose
least fixpointWell-founded Functions and Extreme Predicates in Dafny: A Tutorial
Logistic Supply ChainTowards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving
m
mechanical proof assistantWell-founded Functions and Extreme Predicates in Dafny: A Tutorial
ML PolymorphismImplementing Polymorphism in Zenon
modelThe Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps
monadFunctional Pearl: the Proof Search Monad
n
nbSATOn Reducing Clause DataBase in Glucose
p
Parsing MathematicsImproving Statistical Linguistic Algorithms for Parsing Mathematics
probability theoryTowards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving
proofClausal Proof Compression
proof certificationDefining the meaning of TPTP formatted proofs
proof searchFunctional Pearl: the Proof Search Monad
proofcertDefining the meaning of TPTP formatted proofs
r
Reliability Block DiagramsTowards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving
Representation of sets of equivalent termsA Method to Simplify Expressions: Intuition and Preliminary Experimental Results
s
SATClausal Proof Compression
Simplification of expressionsA Method to Simplify Expressions: Intuition and Preliminary Experimental Results
t
tableau methodImplementing Polymorphism in Zenon
Tarskian GeometryExperiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry
TPTPDefining the meaning of TPTP formatted proofs
The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps
TSTPDefining the meaning of TPTP formatted proofs
type checkingImproving Statistical Linguistic Algorithms for Parsing Mathematics
v
verificationFunctional Pearl: the Proof Search Monad