EasyChair Publications
Search
IWIL-2015 Volume Information
Volume:Boris Konev, Stephan Schulz and Laurent Simon (editors)
IWIL-2015. 11th International Workshop on the Implementation of Logics

IWIL-2015 Volume Information

Title:IWIL-2015. 11th International Workshop on the Implementation of Logics
Editors:Boris Konev, Stephan Schulz and Laurent Simon
Series:EPiC Series in Computing
Volume:40
Publication date:September 27, 2016

Papers

AuthorsTitlePagesPDF
Waqar Ahmed, Osman Hasan and Sofiene TaharTowards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving1-14
Guillaume Bury, Raphaël Cauderlier and Pierre HalmagrandImplementing Polymorphism in Zenon15-20
Marijn Heule and Armin BiereClausal Proof Compression21-26
Cezary Kaliszyk, Josef Urban and Jiri VyskocilImproving Statistical Linguistic Algorithms for Parsing Mathematics27-36
Baudouin Le Charlier and Mêton Mêton AtindehouA Method to Simplify Expressions: Intuition and Preliminary Experimental Results37-51
Rustan LeinoWell-founded Functions and Extreme Predicates in Dafny: A Tutorial52-66
Chu Min Li, Fan Xiao and Ruchu XuOn Reducing Clause DataBase in Glucose67-77
Roberto Blanco, Tomer Libal and Dale MillerDefining the meaning of TPTP formatted proofs78-90
Jonathan ProtzenkoFunctional Pearl: the Proof Search Monad91-105
Geoff Sutcliffe and Stephan SchulzThe Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps106-121
Josef Urban and Robert VeroffExperiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry122-126

Keyphrases

CountKeyphrase
2automated theorem proving, tptp
1automated reasoning, backtracking, boolean calculus, coinduction, coinductive predicate, compression, computational linguistics, dedukti, derivation, equivalence problem, first order logic, flyspeck, glucose, greatest fixpoint, higher order logic, hol light, induction, inductive predicate, interpretation, large theory automated reasoning, learnt clause database, least fixpoint, logistic supply chain, mechanical proof assistant, ml polymorphism, model, monad, nbsat, parsing mathematics, probability theory, proof, proof certification, proof search, proofcert, reliability block diagrams, representation of sets of equivalent terms, sat, simplification of expressions, tableau method, tarskian geometry, tstp, type checking, verification