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

PAAR-2014 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
Volume:31
Publication date:July 5, 2015

Papers

AuthorsTitlePagesPDF
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

Keyphrases

CountKeyphrase
3automated theorem proving
2model finding
1atp competitions, automated reasoning, 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 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