Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
45
views
18
references
Top references
cited by
4
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
2,515
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Automated Deduction - CADE-25
System Description: E.T. 0.1
other
Author(s):
Cezary Kaliszyk
,
Stephan Schulz
,
Josef Urban
,
Jiří Vyskočil
Publication date
(Online):
July 25 2015
Publisher:
Springer International Publishing
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
ScienceOpen Research
Most cited references
18
Record
: found
Abstract
: not found
Article
: not found
The TPTP Problem Library and Associated Infrastructure
Geoff Sutcliffe
(2009)
0
comments
Cited
75
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
First-Order Theorem Proving and Vampire
Laura Kovacs
,
Andrei Voronkov
(2013)
0
comments
Cited
41
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Learning-Assisted Automated Reasoning with Flyspeck
Josef Urban
,
Cezary Kaliszyk
(2014)
0
comments
Cited
41
times
– based on
0
reviews
Review now
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2015
Publication date (Online):
July 25 2015
Pages
: 389-398
DOI:
10.1007/978-3-319-21401-6_27
SO-VID:
6d72657f-64bc-41cf-9ce5-aa198ece3797
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 3
History and Prospects for First-Order Automated Deduction
pp. 29
Stumbling Around in the Dark: Lessons from Everyday Mathematics
pp. 55
Automated Reasoning in the Wild
pp. 73
Automating Leibniz’s Theory of Concepts
pp. 101
Confluence Competition 2015
pp. 105
Termination Competition (termCOMP 2015)
pp. 111
Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent
pp. 127
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
pp. 137
Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies
pp. 152
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
pp. 163
Reducing Relative Termination to Dependency Pair Problems
pp. 181
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
pp. 197
A Decision Procedure for (Co)datatypes in SMT Solvers
pp. 214
Deciding $$\mathsf {ATL^*}$$ Satisfiability by Tableaux
pp. 231
A Formalisation of Finite Automata Using Hereditarily Finite Sets
pp. 246
SEPIA: Search for Proofs Using Inferred Automata
pp. 256
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3
pp. 272
Inductive Beluga: Programming Proofs
pp. 285
SMTtoTPTP – A Converter for Theorem Proving Formats
pp. 295
CTL Model Checking in Deduction Modulo
pp. 311
Quantifier-Free Equational Logic and Prime Implicate Generation
pp. 326
Quantomatic: A Proof Assistant for Diagrammatic Reasoning
pp. 339
Cooperating Proof Attempts
pp. 356
Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
pp. 367
Beagle – A Hierarchic Superposition Theorem Prover
pp. 389
System Description: E.T. 0.1
pp. 399
Playing with AVATAR
pp. 419
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
pp. 434
Exploring Theories with a Model-Finding Assistant
pp. 450
Abstract Interpretation as Automated Deduction
pp. 467
A Uniform Substitution Calculus for Differential Dynamic Logic
pp. 482
Program Synthesis Using Dual Interpretation
pp. 501
Automated Theorem Proving for Assertions in Separation Logic with All Connectives
pp. 517
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS
pp. 539
Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition
pp. 557
Regular Patterns in Second-Order Unification
pp. 572
Theorem Proving with Bounded Rigid E-Unification
pp. 591
Expressing Symmetry Breaking in DRAT Proofs
pp. 607
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
pp. 623
Linear Integer Arithmetic Revisited
Similar content
2,515
E.T. the Extra-Terrestrial
Authors:
S. Spielberg
O uso do P: E.T. (Polietileno Tereftalato) na construção de contenções ortodônticas removíveis
Authors:
M Silveira
,
MR Silveira
B.M. Moores, S.A. Watkinson, E.T. Henshaw and B.J. Pearcy, Editors, Practical Guide to Quality Assurance in Medical Imaging, John Wiley & Sons, Chichester (1987), p. 131 £18.50.
Authors:
D Dance
See all similar
Cited by
4
Monte Carlo Tableau Proof Search
Authors:
Michael Farber
,
Cezary Kaliszyk
,
Josef Urban
ProofWatch: Watchlist Guidance for Large Theories in E
Authors:
Zarathustra Goertzel
,
Jan Jakubův
,
Stephan Schulz
…
Machine Learning Guidance and Proof Certification for Connection Tableau
Authors:
Josef Urban
,
Michael Farber
,
Cezary Kaliszyk
See all cited by