PAAR-2014: Volume Information
Volume:Stephan Schulz, Leonardo De Moura and Boris Konev (editors).
PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning

Volume Information

Title:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Editors:Stephan Schulz, Leonardo De Moura and Boris Konev
Series:EPiC Series in Computing
Publication date:July 5, 2015


Uwe WaldmannHierarchic Superposition Revisited1
Negin Arhami and Geoff SutcliffeThe Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics2-11
Joshua BaxA Model Guided Instantiation Heuristic for the Superposition Calculus with Theories12-24
Maria Paola Bonacina and David PlaistedSGGS Theorem Proving: an Exposition25-38
Simon CruanesLogtk : A Logic ToolKit for Automated Reasoning and its Implementation39-49
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael NorrishBeagle as a HOL4 external ATP method50-59
Cezary Kaliszyk, Josef Urban and Jiri VyskocilMachine Learner for Automated Reasoning 0.4 and 0.560-66
Muhammad Nassar and Geoff SutcliffeAutomated Theorem Proving using the TPTP Process Instruction Language67-75
Salman Saghafi and Daniel DoughertyRazor: Provenance and Exploration in Model-Finding76-93
Sophie Tourret, Mnacho Echenim and Nicolas PeltierA Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses94-104
Daniel WandPolymorphic+Typeclass Superposition105-119


ATP Competitions, automated reasoning, automated theorem proving3, automated theorem proving process, Beagle, constraints, de Bruijn, Description Logics, discrimination tree, EPR, equational logic, first-order logic, formal mathematics, geometric logic, HOL4, instance-based theorem proving, large theories, machine learning, model finding2, model-based theorem proving, polymorphism, prime implicates, Provenance, Quantifier Instantiation, semantic guidance, substitution, superposition, superposition calculus, term representation, theorem proving, TPTP, TPTP Process Instruction language, unification.