Notice
This item was automatically migrated from a legacy system. It's data has not been checked and might not meet the quality criteria of the present system.
Record link: 
http://hdl.handle.net/20.500.12708/57144
-
Title: 
Automated Invention of Strategies and Term Orderings for Vampire
-
Citation: 
Jakubuv, J., Suda, M., & Urban, J. (2017). Automated Invention of Strategies and Term Orderings for Vampire. In GCAI 2017. 3rd Global Conference on Artificial Intelligence (pp. 121–133). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57144
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Authors: 
Jakubuv, Jan 
Suda, Martin 
Urban, Josef 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
GCAI 2017. 3rd Global Conference on Artificial Intelligence 
-
Date (published): 
2017
-
Event name: 
GCAI 2017 / 3rd Global Conference on Artificial Intelligence 
-
Event date: 
19-Oct-2017 - 22-Oct-2017
-
Event place: 
Miami, USA, Non-EU
-
Number of Pages: 
13
-
Publisher: 
EasyChair EPiC Series in Computing, Volume 50
-
Peer reviewed: 
Yes
-
Keywords: 
machine learning; automated theorem proving; first-order logic; proving strategy; strategy invention; parameters learning
-
Abstract: 
In this work we significantly increase the performance of the Vampire and E automated theorem provers (ATPs) on a set of loop theory problems. This is done by developing EmpireTune, an AI system that automatically invents targeted search strategies for Vampire and E. EmpireTune extends previous strategy invention systems in several ways. We have developed support for the Vampire prover, further ex...
en
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
Informatik
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

196
checked on Nov 23, 2023

Google ScholarTM

Check