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

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
Publication date:September 27, 2016


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


automated reasoning, automated theorem proving2, 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, TPTP2, TSTP, type checking, verification.