Home
Publishing
DrugRxiv
Drug Repurposing
Network Medicine
About
REPO4EU
Meet the team
Drug Repurposing Research Collection
Conference
Blog
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Publishing
DrugRxiv
Drug Repurposing
Network Medicine
About
REPO4EU
Meet the team
Drug Repurposing Research Collection
Conference
My ScienceOpen
Sign in
Register
Dashboard
Search
46
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,290
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,290
LAS POSIBILIDADES DE UN DESPIDO OBJETIVO DELART.52.C) E.T. DURANTE UN ERETEMPORAL. COMENTARIO A LA STS DE 12 DE MARZO DE 2014
Authors:
Héctor CLARK SORIANO
Discussion on: ‘Analysis of Closed-Loop Identification with a Tailor-Made Parameterization’ by E.T. van Donkelaar and P.M.J. Van den Hof
Authors:
I.D. Landau
,
A. Karimi
,
F. de Bruyne
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