Last update:
Wed Sep 18 08:29:42 MDT 2024
Larry Wos Editorial: A journal is born . . . . . . 1--3
L. Wos and
Fernando Pereira and
Robert Hong and
Robert S. Boyer and
J. Strother Moore and
W. W. Bledsoe and
L. J. Henschen and
Bruce G. Buchanan and
Graham Wrightson and
Cordell Green An overview of automated reasoning and
related fields . . . . . . . . . . . . . 5--48
James S. Bennett ROGET: A knowledge-based system for
acquiring the conceptual structure of a
diagnostic expert system . . . . . . . . 49--74
Christian Lengauer On the role of automated theorem proving
in the compile-time derivation of
concurrency . . . . . . . . . . . . . . 75--101
Ewing Lusk and
Ross Overbeek Non-horn problems . . . . . . . . . . . 103--114
David M. Russinoff An experiment with the Boyer--Moore
theorem prover: A proof of Wilson's
theorem . . . . . . . . . . . . . . . . 121--139
Adnan Yahya and
Lawrence J. Henschen Deduction in non-Horn databases . . . . 141--160
Peter E. Friedland and
Yumi Iwasaki The concept and implementation of
skeletal plans . . . . . . . . . . . . . 161--208
E. L. Lusk and
R. A. Overbeek Reasoning about equality . . . . . . . . 209--228
Anonymous Announcements . . . . . . . . . . . . . 229--229
Anonymous Changes of address . . . . . . . . . . . 230--230
William McCune and
Lawrence Henschen Experiments with semantic paramodulation 231--261
Alan Bundy Incidence calculus: A mechanism for
probabilistic reasoning . . . . . . . . 263--283
R. L. Constable and
T. B. Knoblock and
J. L. Bates Writing programs that construct proofs 285--326
H. J. Ohlbach and
M. Schmidt-Schauss The lion and the unicorn . . . . . . . . 327--332
Mark E. Stickel Automated deduction by theory resolution 333--355
John G. Mauceri Robot selection expert `Rose' . . . . . 357--390
Jon Doyle Circumscription and implicit
definability . . . . . . . . . . . . . . 391--405
N. Shankar Towards mechanical metamathematics . . . 407--434
Hans Jürgen Ohlbach Predicate logic hacker tricks . . . . . 435--440
Anonymous Announcement . . . . . . . . . . . . . . 441--441
Bruce D. Parrello and
Waldo C. Kabat and
L. Wos Job-shop scheduling using automated
reasoning: A case study of the
car-sequencing problem . . . . . . . . . 1--42
Werner Dilger and
Agnes Janson Intelligent backtracking in deduction
systems by means of extended unification
graphs . . . . . . . . . . . . . . . . . 43--62
Lawrence C. Paulson Proving termination of normalization
functions for conditional expressions 63--74
Wolfram Büttner Unification in datastructure multisets 75--88
Mark E. Stickel Schubert's Steamroller problem:
Formulations and solutions . . . . . . . 89--101
Anonymous Announcing a new journal . . . . . . . . 103--103
Anonymous Addresses of Editor-in-Chief and
Editorial Board . . . . . . . . . . . . 105--107
Alan Bundy Correctness criteria of some algorithms
for uncertain reasoning using Incidence
Calculus . . . . . . . . . . . . . . . . 109--126
Thomas Kramer Automated analysis of operators on state
tables: A technique for intelligent
search . . . . . . . . . . . . . . . . . 127--153
C. Aquilano and
R. Barbuti and
P. Bocchetti and
M. Martelli Negation as Failure. Completeness of the
Query Evaluation Process for Horn clause
programs with recursive definitions . . 155--170
David A. Plaisted A decision procedure for combinations of
propositional temporal logic and other
specialized theories . . . . . . . . . . 171--190
Francis Jeffry Pelletier Seventy-five problems for testing
automatic theorem provers . . . . . . . 191--216
Anonymous Call for papers . . . . . . . . . . . . 217--217
Anonymous Announcing a new journal . . . . . . . . 218--218
J. Strother Moore Editor's preface to `Basic principles of
mechanical theorem proving in elementary
geometries' by Wu Wen-Tsun . . . . . . . 219--220
Wen-Tsun Wu Basic principles of mechanical theorem
proving in elementary geometries . . . . 221--252
Shang-Ching Chou and
William F. Schelter Proving geometry theorems with rewrite
rules . . . . . . . . . . . . . . . . . 253--273
Joerg H. Siekmann Editor's note . . . . . . . . . . . . . 275--275
Manfred Schmidt-Schauss Unification under associativity and
idempotence is of type nullary . . . . . 277--281
Franz Baader The theory of idempotent semigroups is
of unification type zero . . . . . . . . 283--286
Robert Boyer and
Ewing Lusk and
William McCune and
Ross Overbeek and
Mark Stickel and
Lawrence Wos Set theory in first-order logic: Clauses
for Gödel's axioms . . . . . . . . . . . 287--327
Anonymous Editorial announcement A new column:
Basic research problems . . . . . . . . iii--iii
Helder Coelho and
Luis Moniz Pereira Automated reasoning in geometry theorem
proving with Prolog . . . . . . . . . . 329--390
Jia-Huai You and
P. A. Subrahmanyam A class of confluent term rewriting
systems and unification . . . . . . . . 391--418
Barney Glickfeld and
Ross Overbeek A foray into combinatory logic . . . . . 419--431
Anonymous Announcement . . . . . . . . . . . . . . 433--433
Hans Jürgen Ohlbach Link inheritance in abstract clause
graphs . . . . . . . . . . . . . . . . . 1--34
Tie-Cheng Wang and
W. W. Bledsoe Hierarchical deduction . . . . . . . . . 35--77
Larry Wos Editor's note . . . . . . . . . . . . . 79--80
Larry Wos Some obstacles to the automation of
reasoning, and the problem of redundant
information . . . . . . . . . . . . . . 81--90
William McCune and
Larry Wos A case study in automated theorem
proving: Finding sages in combinatory
logic . . . . . . . . . . . . . . . . . 91--107
Anonymous Change of address . . . . . . . . . . . 109--109
Anonymous Announcements . . . . . . . . . . . . . 109--111
Anthony G. Cohn A more expressive formulation of many
sorted logic . . . . . . . . . . . . . . 113--200
Larry Wos The problem of choosing the inference
rule to employ . . . . . . . . . . . . . 201--209
Rick L. Stevens Some experiments in nonassociative ring
theory with an automated theorem prover 211--221
Anonymous Announcement . . . . . . . . . . . . . . 223--223
S. V. Reeves Adding equality to semantic tableaux . . 225--246
Alexander Herold and
Jörg H. Siekmann Unification in Abelian semigroups . . . 247--283
Mark E. Stickel A comparison of the variable-abstraction
and constant-abstraction methods for
associative-commutative unification . . 285--289
Shang-Ching Chou A method for the mechanical derivation
of formulas in elementary geometry . . . 291--299
J.-L. Lassez and
K. Marriott Explicit representation of terms defined
by counter examples . . . . . . . . . . 301--317
Larry Wos The problem of extending the set of
support strategy . . . . . . . . . . . . 319--328
Michael Miller and
Donald Perlis Proving self-utterances . . . . . . . . 329--338
Anonymous Announcements . . . . . . . . . . . . . 339--342
Zohar Manna and
Richard Waldinger How to clear a block: A theory of plans 343--377
Alexander Bockmayr A note on a canonical theory with
undecidable unification and matching
problem . . . . . . . . . . . . . . . . 379--381
Piotr Rudnicki Obvious inferences . . . . . . . . . . . 383--393
Richard Treitel and
Michael R. Genesereth Choosing directions for rules . . . . . 395--431
Larry Wos The problem of definition expansion and
contraction . . . . . . . . . . . . . . 433--435
Tie-Cheng Wang Case studies of $Z$-module reasoning:
Proving benchmark theorems from ring
theory . . . . . . . . . . . . . . . . . 437--451
Anonymous Publisher's announcement . . . . . . . . v--v
Jaakko Hintikka Model minimization--- An alternative to
circumscription . . . . . . . . . . . . 1--13
Alan Bundy and
Leon Sterling Meta-level inference: Two applications 15--27
Paul Helman and
Robert Veroff Designing deductive databases . . . . . 29--68
F. Oppacher and
E. Suen HARP: A tableau-based theorem prover . . 69--100
Larry Wos The problem of finding a strategy to
control binary paramodulation . . . . . 101--107
Anonymous Errata . . . . . . . . . . . . . . . . . 109--111
Anonymous Book received . . . . . . . . . . . . . 113--113
Anonymous Announcements . . . . . . . . . . . . . 115--116
Robert S. Boyer and
J. Strother Moore The addition of bounded quantification
and partial functions to a computational
logic and its theorem prover . . . . . . 117--172
Marek Zaionc Mechanical procedure for proof
construction via closed terms in typed $
\lambda $ calculus . . . . . . . . . . . 173--190
Melvin Fitting First-order modal tableaux . . . . . . . 191--213
Larry Wos The problem of explaining the disparate
performance of hyperresolution and
paramodulation . . . . . . . . . . . . . 215--217
Art Quaife Automated proofs of Löb's theorem and
Gödel's two incompletensess theorems . . 219--231
Ross Overbeek Book review . . . . . . . . . . . . . . 233--234
Anonymous Errata . . . . . . . . . . . . . . . . . 235--236
Anonymous Publisher's announcement . . . . . . . . iii--iii
Shang-Ching Chou An introduction to Wu's method for
mechanical theorem proving in geometry 237--267
Sidney C. Bailin A $ \lambda $-unifiability test for set
theory . . . . . . . . . . . . . . . . . 269--286
David A. Plaisted Non-Horn clause logic programming
without contrapositives . . . . . . . . 287--325
Larry Wos The problem of self-analytically
choosing the set of support . . . . . . 327--329
Deepak Kapur and
Hantao Zhang Proving equivalence of different
axiomatizations of free groups . . . . . 331--352
Mark E. Stickel A prolog technology theorem prover:
Implementation by an extended prolog
compiler . . . . . . . . . . . . . . . . 353--380
Ursula Martin and
Tobias Nipkow Unification in Boolean rings . . . . . . 381--396
Kenneth A. Ross and
Rodney W. Topor Inferring negative information from
disjunctive databases . . . . . . . . . 397--424
Klaus Heje Munch A new reduction rule for the connection
graph proof procedure . . . . . . . . . 425--444
Leonard G. Monk Inference rules using local contexts . . 445--462
Larry Wos The problem of self-analytically
choosing the weights . . . . . . . . . . 463--464
Hans-Jürgen Bürckert and
Alexander Herold and
Deepak Kapur Opening the AC-unification race . . . . 465--474
Anonymous Publisher's announcement . . . . . . . . v--v
Vladimir Lifschitz What is the inverse method? . . . . . . 1--23
Dallas Lankford Non-negative integer basis algorithms
for linear equations with integer
coefficients . . . . . . . . . . . . . . 25--35
D. A. Wolfram Intractable unifiability problems and
backtracking . . . . . . . . . . . . . . 37--47
Tong Gao Tang Temporal logic CTL + PROLOG . . . . . . 49--65
S. Purushothaman and
P. A. Subrahmanyam Mechanical certification of systolic
algorithms . . . . . . . . . . . . . . . 67--91
Larry Wos The problem of finding an inference rule
for set theory . . . . . . . . . . . . . 93--95
Art Quaife Automated development of Tarski's
geometry . . . . . . . . . . . . . . . . 97--118
Anonymous Addresses of Editorial Board . . . . . . 119--121
Anonymous Announcements . . . . . . . . . . . . . 123--124
Robert Boyer Note on verification . . . . . . . . . . 125--125
Avra Cohn The notion of proof in hardware
verification . . . . . . . . . . . . . . 127--139
Tie-Cheng Wang and
Rick Stevens Solving open problems in right
alternative rings with $Z$-module
reasoning . . . . . . . . . . . . . . . 141--165
Teodor C. Przymusinski On the declarative and procedural
semantics of logic programs . . . . . . 167--205
K. S. Leung and
W. Lam A fuzzy expert system shell using both
exact and inexact reasoning . . . . . . 207--233
Larry Wos The problem of determining the size of a
complete set of reductions . . . . . . . 235--237
Cynthia A. Wick and
William W. McCune Automated reasoning about elementary
point-set topology . . . . . . . . . . . 239--255
Peter B. Andrews On connections and higher-order logic 257--291
Arcot Rajasekar and
Jorge Lobo and
Jack Minker Weak Generalized Closed World Assumption 293--307
Ulrich Furbach and
Steffen Hölldobler and
Joachim Schreiber Horn equational theories and
paramodulation . . . . . . . . . . . . . 309--337
Bruce W. Char and
Alan R. Macnaughton and
Paul A. Strooper Discovering inequality conditions in the
analytic solution of optimization
problems . . . . . . . . . . . . . . . . 339--362
Lawrence C. Paulson The foundation of a generic theorem
prover . . . . . . . . . . . . . . . . . 363--397
Larry Wos The problem of guaranteeing the
existence of a complete set of
reductions . . . . . . . . . . . . . . . 399--401
Richard Schmid and
Hans-Albert Schneider and
Thomas Filkorn Using an extended PROLOG to solve the
lion and unicorn puzzle . . . . . . . . 403--408
J. Strother Moore System verification . . . . . . . . . . 409--410
William R. Bevier and
Warren A. Hunt, Jr. and
J. Strother Moore and
William D. Young An approach to systems verification . . 411--428
Warren A. Hunt, Jr. Microprocessor design verification . . . 429--460
J. Strother Moore A mechanically verified language
implementation . . . . . . . . . . . . . 461--492
William D. Young A mechanically verified code generator 493--518
William R. Bevier Kit and the short stack . . . . . . . . 519--530
Larry Wos The problem of guaranteeing the absence
of a complete set of reductions . . . . 531--532
G. H. Chisholm and
B. T. Smith and
A. S. Wojcik An automated reasoning problem
associated with proving claims about
programs using Floyd--Hoare inductive
assertion methods . . . . . . . . . . . 533--540
Yves Auffray and
Jean-Jacques Hebrard Strategies for modal resolution: Results
and problems . . . . . . . . . . . . . . 1--38
Pierre Lescanne On the recursive decomposition ordering
with lexicographical status and other
related orderings . . . . . . . . . . . 39--49
J. W. Roach and
R. Sundararajan and
L. T. Watson Replacing unification by constraint
satisfaction to improve logic program
expressiveness . . . . . . . . . . . . . 51--75
Larry Wos The problem of choosing between logic
programming and general-purpose
automated reasoning . . . . . . . . . . 77--78
Siva Anantharaman and
Jieh Hsiang Automated proofs of the Moufang
identities in alternative rings . . . . 79--109
Anonymous Editorial announcement . . . . . . . . . iii--iii
John Staples and
Peter J. Robinson Structure sharing for quantified terms:
Fundamentals . . . . . . . . . . . . . . 115--145
James J. Lu and
V. S. Subrahmanian Protected completions of first-order
general logic programs . . . . . . . . . 147--172
D. Cantone and
E. G. Omodeo and
A. Policriti The automation of syllogistic . . . . . 173--187
D. Cantone and
V. Cutello Decision procedures for elementary
sublanguages of set theory . . . . . . . 189--201
Giuseppa Carr\`a Ferro and
Giovanni Gallo A procedure to prove statements in
differential geometry . . . . . . . . . 203--209
Larry Wos The problem of finding a mapping between
clause representation and
natural-deduction representation . . . . 211--212
Larry Wos Meeting the challenge of fifty years of
logic . . . . . . . . . . . . . . . . . 213--232
Timothy Stokes Gröbner bases in exterior algebra . . . . 233--250
Yuan Yu Computer proofs in Group Theory . . . . 251--286
W. Bibel Short proofs of the pigeonhole formulas
based on the connection method . . . . . 287--297
Joseph S. Di Piazza Interweaving knowledge extracting,
organizing and evaluating: A concrete
design for preventing logic and
structure bugs while interviewing
experts . . . . . . . . . . . . . . . . 299--317
Hans Kleine Büning and
Ulrich Löwen and
Stefan Schmitgen Equivalence of propositional Prolog
programs . . . . . . . . . . . . . . . . 319--335
Larry Wos The problem of finding a semantic
strategy for focusing inference rules 337--339
W. W. Bledsoe Challenge problems in elementary
calculus . . . . . . . . . . . . . . . . 341--359
Anonymous Publisher's announcement . . . . . . . . iii--iii
Peter F. Patel-Schneider A decidable first-order logic for
knowledge representation . . . . . . . . 361--388
David A. Plaisted A sequent-style model elimination
strategy and a positive refinement . . . 389--402
Xiaoshan Gao Transcendental functions and mechanical
theorem proving in elementary geometries 403--417
John L. Pollock Interest driven suppositional reasoning 419--461
Larry Wos The problem of choosing between
predicate and function notation for
problem representation . . . . . . . . . 463--464
S. Winker Robbins algebra: Conditions that make a
near-boolean algebra boolean . . . . . . 465--489
Anonymous Call for papers . . . . . . . . . . . . 491--492
Anonymous Publisher's announcement . . . . . . . . v--v
Donald W. Loveland Near-Horn Prolog and beyond . . . . . . 1--26
Peter Padawitz Inductive expansion: A calculus for
verifying and synthesizing functional
and logic programs . . . . . . . . . . . 27--103
Larry Wos The problem of finding a restriction
strategy more effective than the set of
support strategy . . . . . . . . . . . . 105--107
Matt Kaufmann Generalization in the presence of free
variables: A mechanically-checked
correctness proof for one algorithm . . 109--158
Rick Stevens Book reviews . . . . . . . . . . . . . . 159--161
Anonymous Errata . . . . . . . . . . . . . . . . . 163--163
Anonymous Addresses of Editorial Board . . . . . . 165--167
Alfredo Ferro Introduction . . . . . . . . . . . . . . 169--170
Wu Wen-Tsun Mechanical theorem proving of
differential geometries and some of its
applications in mechanics . . . . . . . 171--191
D. Cantone Decision procedures for elementary
sublanguages of set theory: X.
Multilevel syllogistic extended by the
singleton and powerset operators . . . . 193--230
D. Cantone and
J. T. Schwartz Decision procedures for elementary
sublanguages of set theory: XI.
Multilevel syllogistic extended by some
elementary map constructs . . . . . . . 231--256
A. Ferro Decision procedures for elementary
sublanguages of set theory: XII.
Multilevel syllogistic extended with
singleton and choice operators . . . . . 257--270
Franco Parlamento and
Alberto Policriti Decision procedures for elementary
sublanguages of set theory: XIII. Model
graphs, reflection and decidability . . 271--284
Peter B. Andrews More on the problem of finding a mapping
between clause representation and
natural-deduction representation . . . . 285--286
Art Quaife Unsolved problems in elementary number
theory . . . . . . . . . . . . . . . . . 287--300
Anonymous A well-kept secret of history . . . . . 301--302
Alan Bundy and
Frank van Harmelen and
Jane Hesketh and
Alan Smaill Experiments with proof plans for
induction . . . . . . . . . . . . . . . 303--324
Rolf Socher Optimizing the clausal normal form
transformation . . . . . . . . . . . . . 325--336
Danny De Schreye and
Bern Martens and
Gunther Sablon and
Maurice Bruynooghe Compiling bottom-up and mixed
derivations into top-down executable
logic programs . . . . . . . . . . . . . 337--358
Allan Ramsay Generating relevant models . . . . . . . 359--368
Werner Nutt The unification hierarchy is undecidable 369--381
Tong Gao Tang Programming in temporal-nonmonotonic
reasoning . . . . . . . . . . . . . . . 383--401
Yishai A. Feldman and
Charles Rich Pattern-directed invocation with
changing equations . . . . . . . . . . . 403--433
Larry Wos The problem of choosing the type of
subsumption to use . . . . . . . . . . . 435--438
Matthew Wilding Proving Matijasevich's lemma with a
default arithmetic strategy . . . . . . 439--446
Michael A. McRobbie Automated reasoning and nonclassical
logics: Introduction . . . . . . . . . . 447--451
John K. Slaney The Ackermann constant theorem: A
computer-assisted investigation . . . . 453--474
Paul Pritchard Algorithms for finding matrix models of
propositional calculi . . . . . . . . . 475--487
Laurent Catach TABLEAUX: A general theorem prover for
modal logics . . . . . . . . . . . . . . 489--510
Dov M. Gabbay and
Frank Kriwaczek A family of goal directed theorem
provers based on conjunction and
implication: Part 1 . . . . . . . . . . 511--536
Dick De Jongh and
Lex Hendriks and
Gerard R. Renardel De Lavalette Computations in fragments of
intuitionistic propositional logic . . . 537--561
A. W. Bollen Relevant logic programming . . . . . . . 563--585
Grigori Mints and
Tanel Tammet Condensed detachment is complete for
relevance logic: A computer-aided proof 587--596
Robert K. Meyer and
Martin W. Bunder and
Lawrence Powers Implementing the `Fool's model' of
combinatory logic . . . . . . . . . . . 597--630
Larry Wos The problem of choosing the
representation, inference rule, and
strategy . . . . . . . . . . . . . . . . 631--634
Paul B. Thistlewaite and
Michael A. McRobbie Approaching hard non-classical problems 635--637
Anonymous Publisher's announcement . . . . . . . . v--v
Anonymous A section is born: Studies in Automated
Reasoning . . . . . . . . . . . . . . . 1--2
David M. Russinoff A mechanical proof of Quadratic
Reciprocity . . . . . . . . . . . . . . 3--21
Anita Jindal and
Ross Overbeek and
Waldo C. Kabat Exploitation of parallel processing for
implementing high-performance deduction
systems . . . . . . . . . . . . . . . . 23--38
Eric Domenjoud A technical note on AC-unification. The
number of minimal unifiers of the
equation $ \alpha x_1 + \cdots + \alpha
x_p \doteq_{AC} \beta y_1 + \cdots +
\beta y_q $ . . . . . . . . . . . . . . 39--44
Larry M. Hines Completeness of a prover for dense
linear orders . . . . . . . . . . . . . 45--75
Shyi-Ming Chen and
Jyh-Sheng Ke and
Jin-Fu Chang An inexact reasoning algorithm based on
fuzzy rule matrix transformations . . . 77--90
Art Quaife Automated deduction in von
Neumann--Bernays--Gödel set theory . . . 91--147
Soumitra Bose and
Edmund M. Clarke and
David E. Long and
Spiro Michaylov Parthenon: A parallel theorem prover for
non-Horn clauses . . . . . . . . . . . . 153--181
R. Letz and
J. Schumann and
S. Bayerl and
W. Bibel SETHEO: A high-performance theorem
prover . . . . . . . . . . . . . . . . . 183--212
Robert Veroff and
Larry Wos The linked inference principle, I: The
formal treatment . . . . . . . . . . . . 213--274
James D. Baker and
Shahriar Zand-Biglari An integral theorem prover and the role
of proof planning . . . . . . . . . . . 275--295
J. C. Shepherdson SLDNF-resolution with equality . . . . . 297--306
Larry Wos The problem of choosing between using
and avoiding equality predicates . . . . 307--309
Dave Barker-Plummer Gazing: An approach to the problem of
definition and lemma use . . . . . . . . 311--344
Chitta R. Baral and
V. S. Subrahmanian Stable and extension class theory for
logic programs and default logics . . . 345--366
Robert J. Hall Comparing parameter schemes for
propositional reasoning: An empirical
study . . . . . . . . . . . . . . . . . 367--394
Mark F. Russo and
Richard L. Peskin Automatically identifying the asymptotic
behavior of nonlinear singularly
perturbed boundary value problems . . . 395--419
Larry Wos The problem of reasoning from
inequalities . . . . . . . . . . . . . . 421--426
William W. Mccune Automated discovery of new
axiomatizations of the left group and
right group calculi . . . . . . . . . . 1--24
Shie-Jue Lee and
David A. Plaisted Eliminating duplication with the
hyper-linking strategy . . . . . . . . . 25--42
Dan Benanav Recognizing unnecessary clauses in
resolution based systems . . . . . . . . 43--76
Rolf Socher-Ambrosius How to avoid the derivation of redundant
clauses in reasoning systems . . . . . . 77--97
Nicola Olivetti Tableaux and sequent calculus for
minimal entailment . . . . . . . . . . . 99--139
Larry Wos The problem of demodulation during
inference rule application . . . . . . . 141--143
Larry Wos Note on McCune's article on
discrimination trees . . . . . . . . . . 145--146
William McCune Experiments with discrimination-tree
indexing and path indexing for term
retrieval . . . . . . . . . . . . . . . 147--167
Mark Franzen Hilbert's tenth problem is of
unification type zero . . . . . . . . . 169--178
Michael Kifer and
Eliezer L. Lozinskii A logic for reasoning with inconsistency 179--215
Donald E. Brown and
Wendy J. Markert Uncertainty management with imprecise
knowledge with application to design . . 217--230
Nevin Heintze and
Spiro Michaylov and
Peter Stuckey CLP(\mathfrakR) and some electrical
engineering problems . . . . . . . . . . 231--260
Deepak Kapur and
Paliath Narendran Complexity of unification problems with
associative-commutative operators . . . 261--288
Larry Wos The problem of demodulator adjunction 289--290
Larry Wos Transition to the future . . . . . . . . iii--iii
Kenneth Kunen Single axioms for groups . . . . . . . . 291--308
Arnon Avron and
Furio Honsell and
Ian A. Mason and
Robert Pollack Using typed lambda calculus to implement
formal systems on a machine . . . . . . 309--354
Matt Kaufmann An extension of the Boyer--Moore Theorem
Prover to support first-order
quantification . . . . . . . . . . . . . 355--372
Jean-Louis Lassez and
Michael J. Maher On Fourier's algorithm for linear
arithmetic constraints . . . . . . . . . 373--379
G. M. Kuper and
K. W. McAloon and
K. V. Palem and
K. J. Perry A note on the parallel complexity of
anti-unification . . . . . . . . . . . . 381--389
Arthur L. Delcher and
Simon Kasif Efficient parallel term matching and
anti-unification . . . . . . . . . . . . 391--406
Larry Wos The problem of demodulating across
argument and literal boundaries . . . . 407--408
Simon Parsons Book review . . . . . . . . . . . . . . 409--411
William W. McCune Single axioms for groups and Abelian
groups with various operations . . . . . 1--13
P. A. J. Noel Experimenting with Isabelle in ZF set
theory . . . . . . . . . . . . . . . . . 15--58
Thomas J. Weigert and
Jing-Pha Tsai and
Xuhua Liu Fuzzy operator logic and fuzzy
resolution . . . . . . . . . . . . . . . 59--78
F. Corella What holds in a context? . . . . . . . . 79--93
Jim Christian Flatterms, discrimination nets, and fast
term rewriting . . . . . . . . . . . . . 95--113
Frank Vlach Simplification in a satisfiability
checker for VLSI applications . . . . . 115--136
Larry Wos The problem of automated theorem finding 137--138
Li Yan Yuan and
Jia-Huai You Autoepistemic circumscription and logic
programming . . . . . . . . . . . . . . 143--160
Shang-Ching Chou and
Xiao-Shan Gao Automated reasoning in differential
geometry and mechanics using the
characteristic set method . . . . . . . 161--172
Shang-Ching Chou and
Xiao-Shan Gao Automated reasoning in differential
geometry and mechanics using the
characteristic set method . . . . . . . 173--189
Raymond Ng and
V. S. Subrahmanian A semantical framework for supporting
subjective and conditional probabilities
in deductive databases . . . . . . . . . 191--235
Marek A. Suchenek First-order syntactic characterizations
of minimal entailment, domain-minimal
entailment, and Herbrand entailment . . 237--263
Arnon Avron Gentzen-type systems, resolution and
tableaux . . . . . . . . . . . . . . . . 265--281
Larry Wos The problem of selecting an approach
based on prior success . . . . . . . . . 283--284
Charles Ashbacher Book review . . . . . . . . . . . . . . 285--286
Larry Wos The kernel strategy and its use for the
study of combinatory logic . . . . . . . 287--343
James J. Lu and
Monica D. Barback and
Lawrence J. Henschen Interpreting disjunctive logic programs
based on a strong sense of disjunction 345--370
James J. Lu and
V. S. Subrahmanian Completeness issues in RUE--NRF
deduction: The undecidability of
viability . . . . . . . . . . . . . . . 371--388
Joachim Steinbach Simplification orderings: Putting them
to the test . . . . . . . . . . . . . . 389--397
Chitta R. Baral and
V. S. Subrahmanian Dualities between alternative semantics
for logic programming and nonmonotonic
reasoning . . . . . . . . . . . . . . . 399--420
Larry Wos The problem of reasoning by analogy . . 421--422
Anonymous Announcement . . . . . . . . . . . . . . 423--423
Adrian Walker Backchain iteration: Towards a practical
inference method that is simple enough
to be proved terminating, sound, and
complete . . . . . . . . . . . . . . . . 1--22
Fausto Giunchiglia and
Toby Walsh The inevitability of inconsistent
abstract spaces . . . . . . . . . . . . 23--41
Amy Felty Implementing tactics and tacticals in a
higher-order logic programming language 43--81
Alberto Segre and
Daniel Scharstein Bounded-overhead caching for
definite-clause theorem proving . . . . 83--113
Gopalan Nadathur A proof procedure for the logic of
hereditary Harrop formulas . . . . . . . 115--145
Larry Wos The problem of naming and function
replacement . . . . . . . . . . . . . . 147--148
Klaus U. Schulz Word unification and transformation of
generalized equations . . . . . . . . . 149--184
Alexandre Boudet Competing for the AC--Unification Race 185--212
William M. Farmer and
Joshua D. Guttman and
F. Javier Thayer IMPS: An interactive mathematical proof
system . . . . . . . . . . . . . . . . . 213--248
John Grant and
John Horty and
Jorge Lobo and
Jack Minker View updates in stratified disjunctive
databases . . . . . . . . . . . . . . . 249--267
Jinchang Wang Inference flexibility in Horn clause
knowledge bases and the simplex method 269--288
Larry Wos The problem of reasoning by case
analysis . . . . . . . . . . . . . . . . 289--291
W. W. Bledsoe and
Guohui Feng SET-VAR . . . . . . . . . . . . . . . . 293--314
Ross Overbeek The CADE-11 competitions: A personal
view . . . . . . . . . . . . . . . . . . 315--316
Ewing L. Lusk and
William W. McCune Uniform strategies: The CADE-11 theorem
proving contest . . . . . . . . . . . . 317--331
Hantao Zhang Automated proofs of equality problems in
Overbeek's competition . . . . . . . . . 333--351
Lawrence C. Paulson Set theory for verification: I. From
foundations to functions . . . . . . . . 353--389
Sidney C. Bailin and
Dave Barker-Plummer $-$-match: An inference rule for
incrementally elaborating set
instantiations . . . . . . . . . . . . . 391--428
Simon Parsons Book review . . . . . . . . . . . . . . 429--431
Larry Wos The problem of induction . . . . . . . . 433--434
Eliezer L. Lozinskii Resolving contradictions: A plausible
semantics for inconsistent systems . . . 1--31
J. Strother Moore Introduction to the OBDD algorithm for
the ATP community . . . . . . . . . . . 33--45
Taäieb Mellouli TMPR: A tree-structured modified problem
reduction proof procedure and its
extension to three-valued logic . . . . 47--87
Belaid Benhamou and
Lakhdar Sais Tractability through symmetries in
propositional calculus . . . . . . . . . 89--102
J. Stuart Aitken and
Han Reichgelt and
Nigel Shadbolt Resolution theorem proving in reified
modal logics . . . . . . . . . . . . . . 103--129
Simon Parsons Book review . . . . . . . . . . . . . . 131--132
Larry Wos The problem of strategy and
hyperresolution . . . . . . . . . . . . 133--134
Ralph M. Butler and
Ross A. Overbeek Formula databases for high-performance
resolution/paramodulation systems . . . 139--156
Timothy S. C. Chou and
Marianne Winslett A model-based belief revision system . . 157--208
E. K. Burke Unification in partially commutative
semigroups . . . . . . . . . . . . . . . 209--223
Maria Paola Bonacina and
Jieh Hsiang On subsumption in distributed
derivations . . . . . . . . . . . . . . 225--240
Vincent J. Digricoli The rue theorem-proving system: The
complete set of LIM+ challenge problems 241--264
Larry Wos The problem of hyperparamodulation . . . 265--271
Tanel Tammet Proof strategies in linear logic . . . . 273--304
Louiqa Raschid and
Jorge Lobo A semantics for a class of
non-deterministic and causal production
system programs . . . . . . . . . . . . 305--349
Giuseppa Carra' Ferro An extension of a procedure to prove
statements in differential geometry . . 351--358
Shie-Jue Lee and
Chih-Hung Wu Improving the efficiency of a
hyperlinking-based theorem prover by
incremental evaluation with network
structures . . . . . . . . . . . . . . . 359--388
Zhenyu Qian and
Tobias Nipkow Reduction and unification in lambda
calculi with a general notion of subtype 389--406
Larry Wos The problem of hyperparamodulation and
nuclei . . . . . . . . . . . . . . . . . 407--409
Anonymous Errata . . . . . . . . . . . . . . . . . 411--412
Maria Paola Bonacina and
Jieh Hsiang Parallelization of deduction strategies:
An analytical study . . . . . . . . . . 1--33
Piero A. Bonatti Autoepistemic logic programming . . . . 35--67
Li-Yan Yuan Autoepistemic logic of first order and
its expressive power . . . . . . . . . . 69--82
C. A. Johnson On the termination of clause graph
resolution . . . . . . . . . . . . . . . 83--115
Adnan Yahya and
José Alberto Fernández and
Jack Minker Ordered model trees: A normal form for
disjunctive deductive databases . . . . 117--143
Chiaki Sakama and
Katsumi Inoue An alternative approach to the semantics
of disjunctive logic programs and
deductive databases . . . . . . . . . . 145--172
Graham Wrightson Preface to the special issue on tableaux 173--173
Melvin Fitting Tableaux for logic programming . . . . . 175--188
Mark E. Stickel Upside-down meta-interpretation of the
model elimination theorem-proving
procedure for deduction and abduction 189--210
Reiner Hähnle and
Peter H. Schmitt The liberalized $ \delta $-rule in free
variable semantic tableaux . . . . . . . 211--221
Vincent Risch and
Camilla B. Schwind Tableau-based characterization and
theorem proving for default logic . . . 223--242
Marcello D'Agostino and
Dov M. Gabbay A generalization of analytic deduction
via labelled deductive systems. Part I:
Basic substructural logics . . . . . . . 243--281
Owen Astrachan METEOR: Exploring model elimination
theorem proving . . . . . . . . . . . . 283--296
R. Letz and
K. Mayr and
C. Goller Controlled integration of the cut rule
into connection tableau calculi . . . . 297--337
Peter Baumgartner and
Ulrich Furbach Model elimination without
contrapositives and its application to
PTTP . . . . . . . . . . . . . . . . . . 339--359
Pierangelo Miglioli and
Ugo Moscato and
Mario Ornaghi An improved refutation system for
intuitionistic predicate logic . . . . . 361--373
Sven Lorenz A tableau prover for domain minimization 375--390
Regimantas Pliu\vskevi\vcius The saturated tableaux for linear
miniscoped Horn-like temporal logic . . 391--407
J. Schumann Tableau-based theorem provers: Systems
and implementations . . . . . . . . . . 409--421
Vladimir Lifschitz Preface to the special issue on
commonsense and nonmonotonic reasoning 1--1
Ilkka Niemelä A decision method for nonmonotonic
reasoning based on autoepistemic
reasoning . . . . . . . . . . . . . . . 3--42
Matthew L. Ginsberg Modality and interrupts . . . . . . . . 43--91
José Júlio Alferes and
Carlos Viegas Damásio and
Luís Moniz Pereira A logic programming system for
nonmonotonic reasoning . . . . . . . . . 93--147
Franz Baader and
Bernhard Hollunder Embedding defaults into terminological
knowledge representation formalisms . . 149--180
Adel Bouhoula and
Michaël Rusinowitch Implicit induction in conditional
theories . . . . . . . . . . . . . . . . 189--235
Allan Ramsay Theorem proving for intensional logic 237--255
Shang-Ching Chou and
Xiao-Shan Gao and
Jing-Zhong Zhang Automated production of traditional
proofs in solid geometry . . . . . . . . 257--291
Deepak Kapur and
G. Sivakumar and
Hantao Zhang A path ordering for proving termination
of AC rewrite systems . . . . . . . . . 293--316
Kumar V. Vadaparty On the complexity of nested-object
matching . . . . . . . . . . . . . . . . 317--323
Donald W. Loveland and
David W. Reed and
Debra S. Wilson SATCHMORE: SATCHMO with RElevancy . . . 325--351
Karl Schlechta Logic, topology, and integration . . . . 353--381
Joan Hart and
Kenneth Kunen Single axioms for odd exponent groups 383--412
Thomas Jech OTTER experiments in a system of
combinatory logic . . . . . . . . . . . 413--426
I. Chakrabarti and
D. Sarkar and
A. K. Majumdar Identification of inductive properties
during verification of synchronous
sequential circuits . . . . . . . . . . 427--462
Vladimir Lifschitz Preface to the special issue on
commonsense and nonmonotonic reasoning v--v
Michael Thielscher and
Torsten Schaub Default reasoning by deductive planning 1--40
Franz Baader and
Bernhard Hollunder Priorities on defaults with
prerequisites, and their application in
treating specificity in terminological
default logic . . . . . . . . . . . . . 41--68
Sakthi Subramanian Mechanical verification of strategies 69--93
T. Schaub A new methodology for query answering in
default logics via structure-oriented
theorem proving . . . . . . . . . . . . 95--165
Lawrence C. Paulson Set theory for verification. II:
Induction and recursion . . . . . . . . 167--215
Kenneth Kunen A Ramsey theorem in Boyer--Moore logic 217--235
Andrei Voronkov The anatomy of vampire . . . . . . . . . 237--265
Hans Jürgen Ohlbach and
Christoph Weidenbach A note on assumptions about Skolem
functions . . . . . . . . . . . . . . . 267--275
Anonymous The Kluwer \LaTeX style file . . . . . . 277--278
Larry Wos Searching for circles of pure proofs . . 279--315
G. D'Agostino and
A. Montanari and
A. Policriti A set-theoretic translation method for
polymodal logics . . . . . . . . . . . . 317--337
Bernhard Beckert and
Joachim Posegga lean TAP: Lean tableau-based deduction 339--358
J. N. Hooker and
V. Vinay Branching rules for satisfiability . . . 359--383
Hantao Zhang Preface to the special issue on
Automated Mathematical induction . . . . 1--1
François Bronsard and
Uday S. Reddy and
Robert W. Hasker Induction using term orders . . . . . . 3--37
Deepak Kapur and
M. Subramaniam New uses of linear arithmetic in
automated theorem proving by induction 39--78
Andrew Ireland and
Alan Bundy Productive use of failure in inductive
proof . . . . . . . . . . . . . . . . . 79--111
Ina Kraan and
David Basin and
Alan Bundy Middle-out reasoning for synthesis and
induction . . . . . . . . . . . . . . . 113--145
David A. Basin and
Toby Walsh A calculus for and termination of
rippling . . . . . . . . . . . . . . . . 147--180
Matt Kaufmann and
Paolo Pecchiari Interaction with the Boyer--Moore
theorem prover: A tutorial study using
the arithmetic--geometric mean theorem 181--222
Robert Veroff Using hints to increase the
effectiveness of an automated reasoning
program: Case studies . . . . . . . . . 223--239
Peter Baumgartner Linear and unit-resulting refutations
for Horn theories . . . . . . . . . . . 241--319
Peter B. Andrews and
Matthew Bishop and
Sunil Issar and
Dan Nesmith and
Frank Pfenning and
Hongwei Xi TPS: A theorem-proving system for
classical type theory . . . . . . . . . 321--353
Lusheng Wang and
S. K. M. Wong and
Y. Y. Yao On the completeness of incidence
calculus . . . . . . . . . . . . . . . . 355--368
Michael Hedberg A type-theoretic interpretation of
constructive domain theory . . . . . . . 369--425
Charles Ashbacher From logic to logic programming . . . . 427--427
Jian Zhang Constructing finite algebras with FALCON 1--22
Larry Wos The power of combining resonance with
heat . . . . . . . . . . . . . . . . . . 23--81
Kenneth Kunen The semantics of answer literals . . . . 83--95
Philippe Codognet and
Daniel Diaz A simple and efficient boolean solver
for Constraint Logic Programming . . . . 97--128
Paliath Narendran and
Michaël Rusinowitch Any ground associative-commutative
theory has a finite canonical system . . 131--143
S. Linton and
D. Shand Some group theoretic examples with
completion theorem provers . . . . . . . 145--169
José Alberto Fernández and
John Grant and
Jack Minker Model theoretic approach to view updates
in deductive databases . . . . . . . . . 171--197
Michael Thielscher On the completeness of SLDENF-resolution 199--214
Larry Wos OTTER and the Moufang identity problem 215--257
Yannis Dimopoulos On computing logic programs . . . . . . 259--289
Lawrence C. Paulson and
Krzysztof Grabczewski Mechanizing set theory . . . . . . . . . 291--323
Shang-Ching Chou and
Xiao-Shan Gao and
Jing-Zhong Zhang Automated generation of readable proofs
with geometric invariants . . . . . . . 325--347
Shang-Ching Chou and
Xiao-Shan Gao and
Jing-Zhong Zhang Automated generation of readable proofs
with geometric invariants . . . . . . . 349--370
Gregory Sidebottom and
William S. Havens Nicolog: A simple yet powerful cc(FD)
language . . . . . . . . . . . . . . . . 371--403
Larry Hines A Tribute to Woody Bledsoe . . . . . . . 1--4
Rong-Huei Hou and
Tzung-Pei Hong and
Shian-Shyong Tseng and
Sy-Yen Kuo A New Probabilistic Induction Method . . 5--24
Grigoris Antoniou and
Elmar Langetepe A Correct Logic Programming Computation
of Default Logic Extensions . . . . . . 25--46
Anavai Ramesh and
Bernhard Beckert and
Reiner Hähnle and
Neil V. Murray Fast Subsumption Checks Using Anti-Links 47--83
Simon Finn and
Michael P. Fourman and
John Longley Partial Functions in a Total Setting . . 85--104
Li Dafa Unification Algorithms for Eliminating
and Introducing Quantifiers in Natural
Deduction Automated Theorem Proving . . 105--134
Francis Jeffry Pelletier and
Geoff Sutcliffe An Erratum for Some Errata to ATP
Problems . . . . . . . . . . . . . . . . 135--135
Geoff Sutcliffe and
Christian Suttner The CADE-13 ATP System Competition . . . 137--138
Christian Suttner and
Geoff Sutcliffe The Design of the CADE-13 ATP System
Competition . . . . . . . . . . . . . . 139--162
Geoff Sutcliffe and
Christian Suttner The Procedures of the CADE-13 ATP System
Competition . . . . . . . . . . . . . . 163--169
Robert Nieuwenhuis and
José Miguel Rivero and
Miguel Ángel Vallejo Barcelona . . . . . . . . . . . . . . . 171--176
Geoffrey D. Alexander CLIN-E --- Smallest Instance First
Hyper-Linking . . . . . . . . . . . . . 177--182
Heng Chu and
David A. Plaisted CLIN-S --- A Semantically Guided
First-Order Theorem Prover . . . . . . . 183--188
Jörg Denzinger and
Martin Kronenburg and
Stephan Schulz DISCOUNT --- A Distributed and Learning
Equational Prover . . . . . . . . . . . 189--198
Tanel Tammet Gandalf . . . . . . . . . . . . . . . . 199--204
Reinhold Letz LINUS --- A Link Instantion Prover with
Unit Support . . . . . . . . . . . . . . 205--210
William McCune and
Larry Wos Otter- The CADE-13 Competition
Incarnations . . . . . . . . . . . . . . 211--220
M. Paramasivam and
David A. Plaisted RRTP --- A Replacement Rule Theorem
Prover . . . . . . . . . . . . . . . . . 221--226
Tim Geisler and
Sven Panne and
Heribert Schütz Satchmo- The Compiling and Functional
Variants . . . . . . . . . . . . . . . . 227--236
Max Moser and
Ortrun Ibens and
Reinhold Letz and
Joachim Steinbach and
Christoph Goller and
Johann Schumann and
Klaus Mayr SETHEO and E-SETHEO --- The CADE-13
Systems . . . . . . . . . . . . . . . . 237--246
Christoph Weidenbach SPASS --- Version 0.49 . . . . . . . . . 247--252
Christian B. Suttner SPTHEO --- A Parallel Theorem Prover . . 253--258
Steve Greenbaum Violet . . . . . . . . . . . . . . . . . 259--264
Thomas Hillenbrand and
Arnim Buch and
Roland Vogt WALDMEISTER --- High-Performance
Equational Deduction . . . . . . . . . . 265--270
Geoff Sutcliffe and
Christian Suttner The Results- of the CADE-13 ATP System
Competition . . . . . . . . . . . . . . 271--286
Francis Jeffry Pelletier and
Geoff Sutcliffe and
Christian Suttner Conclusions about the CADE-13 ATP System
Competition . . . . . . . . . . . . . . 287--296
Patrick Doherty and
Witold \Lukaszewicz and
Andrzej Sza\las Computing Circumscription Revisited: A
Reduction Algorithm . . . . . . . . . . 297--336
Anavai Ramesh and
George Becker and
Neil V. Murray CNF and DNF Considered Harmful for
Computing Prime Implicants\slash
Implicates . . . . . . . . . . . . . . . 337--356
Marek A. Suchenek Evaluation of Queries under Closed-World
Assumption . . . . . . . . . . . . . . . 357--398
Dieter Hutter Coloring Terms to Control Equational
Reasoning . . . . . . . . . . . . . . . 399--442
Jürgen Giesl Termination of Nested and Mutually
Recursive Algorithms . . . . . . . . . . 1--29
C. A. Johnson Deduction Trees and the View Update
Problem in Indefinite Deductive
Databases . . . . . . . . . . . . . . . 31--85
Paliath Narendran and
Friedrich Otto Single Versus Simultaneous Equational
Unification and Equational Unification
for Variable-Permuting Theories . . . . 87--115
O. L. Astrachan and
D. W. Loveland The Use of Lemmas in the Model
Elimination Procedure . . . . . . . . . 117--141
Marc-Michel Corsini and
Antoine Rauzy Toupie: The $ \mu $-calculus over Finite
Domains as a Constraint Language . . . . 143--171
K. Hörwein Structuring Resolution Proofs by
Introducing New Lemmata . . . . . . . . 173--203
Peter Baumgartner and
Stefan Brüning A Disjunctive Positive Refinement of
Model Elimination and its Application to
Subsumption Deletion . . . . . . . . . . 205--262
William Mccune Solution of the Robbins Problem . . . . 263--276
Ricardo Caferra and
Nicolas Peltier A New Technique for Verifying and
Correcting Logic Programs . . . . . . . 277--318
Alan Bundy and
Fausto Giunchiglia and
Adolfo Villafiorita and
Toby Walsh Abstract Proof Checking: An Example
Motivated by an Incompleteness Theorem 319--346
David Sturgill and
Alberto Maria Segre Nagging: A Distributed, Adversarial
Search-Pruning Technique Applied to
First-Order Inference . . . . . . . . . 347--376
José Júlio Alferes and
Luís Moniz Pereira Preface . . . . . . . . . . . . . . . . 1--3
Hans de Nivelle An Algorithm for the Retrieval of
Unifiers from Discrimination Trees . . . 5--25
Gilles Défourneaux and
Christophe Bourely and
Nicolas Peltier Semantic Generalizations for Proving and
Disproving Conjectures by Analogy . . . 27--45
Anatoli Degtyarev and
Andrei Voronkov What You Always Wanted to Know about
Rigid E-Unification . . . . . . . . . . 47--80
Peter Fröhlich and
Wolfgang Nejdl and
Michael Schroeder Strategies in Model-based Diagnosis . . 81--105
José Júlio Alferes and
Luís Moniz Pereira and
Teodor C. Przymusinski 'Classical' Negation in Nonmonotonic
Reasoning and Logic Programming . . . . 107--142
Stefan Brass and
Jürgen Dix Characterizations of the Disjunctive
Well-Founded Semantics: Confluent
Calculi and Iterated GCWA . . . . . . . 143--165
Paola Forcheri and
Paolo Gentilini and
Maria Teresa Molfino Informational Logic as a Tool for
Automated Reasoning . . . . . . . . . . 167--190
Ph. Besnard and
T. Schaub Signed Systems for Paraconsistent
Reasoning . . . . . . . . . . . . . . . 191--213
Guoxiang Huang and
Dale Myers Subgoal Strategies for Solving Board
Puzzles . . . . . . . . . . . . . . . . 215--253
Erica Melis The Heine--Borel Challenge Problem. In
Honor of Woody Bledsoe . . . . . . . . . 255--282
Kahlil Hodgson Shortest Single Axioms for the
Equivalential Calculus with CD and RCD 283--316
Hans Jürgen Ohlbach Elimination of Self-Resolving Clauses 317--336
M. Paramasivam and
David A. Plaisted Automated Deduction Techniques for
Classification in Description Logic
Systems . . . . . . . . . . . . . . . . 337--364
Abdelilah Kandri Rody and
Hamid Maârouf and
Mohamed Ssafini Triviality and Dimension of a System of
Algebraic Differential Equations . . . . 365--385
Anonymous The Eleventh International Conference on
Industrial and Engineering Applications
of Artificial Intelligence and Expert
Systems (IEA/AIE--98) . . . . . . . . . 387--387
Li Hongbo and
Cheng Minteh Clifford Algebraic Reduction Method for
Automated Theorem Proving in
Differential Geometry . . . . . . . . . 1--21
Hoon Hong and
Dalibor Jaku\vs Testing Positiveness of Polynomials . . 23--38
James J. Lu and
Neil V. Murray and
Erik Rosenthal A Framework for Automated Reasoning in
Multiple-Valued Logics . . . . . . . . . 39--67
Kenneth Kunen Nonconstructive Computational
Mathematics . . . . . . . . . . . . . . 69--97
Christian Suttner and
Geoff Sutcliffe The CADE-14 ATP System Competition . . . 99--134
Larry Wos Automating the Search for Elegant Proofs 135--175
Geoff Sutcliffe and
Christian Suttner The TPTP Problem Library . . . . . . . . 177--203
Andrei Voronkov Proof Search in Intuitionistic Logic
with Equality, or Back to Simultaneous
Rigid $E$-Unification . . . . . . . . . 205--231
Jacques Chazarain and
Serge Muller Automated Synthesis of Recursive
Programs from a $ \forall \exists $
Logical Specification . . . . . . . . . 233--275
Anonymous Announcements . . . . . . . . . . . . . 277--277
Deepak Kapur and
Dongming Wang Preface . . . . . . . . . . . . . . . . 277--278
John Harrison and
L. Théry A Skeptic's Approach to Combining HOL
and Maple . . . . . . . . . . . . . . . 279--294
Andrej Bauer and
Edmund Clarke and
Xudong Zhao Analytica-- An Experiment in Combining
Theorem Proving and Symbolic Computation 295--325
Manfred Kerber and
Michael Kohlhase and
Volker Sorge Integrating Computer Algebra into Proof
Planning . . . . . . . . . . . . . . . . 327--355
Andreas Dolzmann and
Thomas Sturm and
Volker Weispfenning A New Approach for Automatic Theorem
Proving in Real Geometry . . . . . . . . 357--380
Jinzhao Wu and
Zhuojun Liu Well-Behaved Inference Rules for
First-Order Theorem Proving . . . . . . 381--400
Larry Wos and
Gail W. Pieper The Hot List Strategy . . . . . . . . . 1--44
Frieder Stolzenburg An Algorithm for General Set Unification
and Its Complexity . . . . . . . . . . . 45--63
Peter Madden and
Alan Bundy and
Alan Smaill Recursive Program Optimization through
Inductive Synthesis Proof Transformation 65--115
Erica Melis and
Jon Whittle Analogy in Inductive Theorem Proving . . 117--147
A. K. Shiny and
Arun K. Pujari An Efficient Algorithm to Generate Prime
Implicants . . . . . . . . . . . . . . . 149--170
William E. Aitken and
Robert L. Constable and
Judith L. Underwood Metalogical Frameworks II: Developing a
Reflected Decision Procedure . . . . . . 171--221
Leon \Lukaszewicz Triple Dots in a Formal Language . . . . 223--239
Gilles Pesant and
Michel Boyer Reasoning about Solids Using Constraint
Logic Programming . . . . . . . . . . . 241--262
Ofer Arieli and
Arnon Avron A Model-Theoretic Approach for
Recovering Consistent Data from
Inconsistent Knowledge Bases . . . . . . 263--309
Johan G. F. Belinfante Computer Proofs in Gödel's Class Theory
with Equational Definitions for
Composite and Cross . . . . . . . . . . 311--339
Johan G. F. Belinfante On Computer-Assisted Proofs in Ordinal
Number Theory . . . . . . . . . . . . . 341--378
Renate A. Schmidt Decidability by Resolution for
Propositional Modal Logics . . . . . . . 379--396
Christian B. Suttner SPS-Parallelism + SETHEO = SPTHEO . . . 397--431
Andrea Formisano and
Alberto Policriti $T$-Resolution: Refinements and Model
Elimination . . . . . . . . . . . . . . 433--483
Anonymous Author Index to Volume 22 . . . . . . . 485--486
Anonymous Subject Index to Volume 22 . . . . . . . 487--487
Anonymous Contents to Volume 22 . . . . . . . . . 489--490
G. Sutcliffe and
C. B. Suttner The CADE-15 ATP System Competition . . . 1--23
Masahito Kurihara and
Hisashi Kondo Completion for Multiple Reduction
Orderings . . . . . . . . . . . . . . . 25--42
John D. Ramsdell The Tail-Recursive SECD Machine . . . . 43--62
T. Recio and
M. P. Vélez Automatic Discovery of Theorems in
Elementary Geometry . . . . . . . . . . 63--82
Alexander Brodsky and
Catherine Lassez and
Jean-Louis Lassez and
Michael J. Maher Separability of Polyhedra for Optimal
Filtering of Spatial and Constraint Data 83--104
Anonymous Announcements . . . . . . . . . . . . . 105--105
Miki Hermann and
Phokion G. Kolaitis Computational Complexity of Simultaneous
Elementary Matching Problems . . . . . . 107--136
Allen Van Gelder Autarky Pruning in Propositional Model
Elimination Reduces Failure Redundancy 137--193
Anonymous Preface . . . . . . . . . . . . . . . . 195--196
Piotr Rudnicki and
Andrzej Trybulec On Equivalents of Well-Foundedness . . . 197--234
Florian Kammüller and
Lawrence C. Paulson A Formal Proof of Sylow's Theorem . . . 235--264
Ching-Tsun Chou and
Doron Peled Formal Verification of a Partial-Order
Reduction Technique for Model Checking 265--298
Wolfgang Naraschewski and
Tobias Nipkow Type Inference Verified: Algorithm W in
Isabelle/HOL . . . . . . . . . . . . . . 299--318
Catherine Dubois and
Valérie Ménissier-Morain Certification of a Type Inference Tool
for ML: Damas--Milner within Coq . . . . 319--346
M. Jaume A Full Formalization of SLD--Resolution
in the Calculus of Inductive
Constructions . . . . . . . . . . . . . 347--371
James McKinna and
Robert Pollack Some Lambda Calculus and Type Theory
Formalized . . . . . . . . . . . . . . . 373--409
Bernhard Reus Formalizing Synthetic Domain Theory . . 411--444
David M. Goldschlag A Mechanization of Unity in PC--NQTHM-92 445--498
Ian P. Gent and
Toby Walsh Satisfiability in the Year 2000 . . . . 1--3
Miron Abramovici and
Jose T. De Sousa A SAT Solver Using Reconfigurable
Hardware and Virtual Logic . . . . . . . 5--36
Etienne de Klerk and
Hans van Maaren and
Joost P. Warners Relaxations of the Satisfiability
Problem Using Semidefinite Programming 37--65
Carla P. Gomes and
Bart Selman and
Nuno Crato and
Henry Kautz Heavy-Tailed Phenomena in Satisfiability
and Constraint Satisfaction Problems . . 67--100
Jan Friso Groote and
Joost P. Warners The Propositional Formula Checker
HeerHugo . . . . . . . . . . . . . . . . 101--125
Edward A. Hirsch SAT Local Search Algorithms: Worst-Case
Study . . . . . . . . . . . . . . . . . 127--143
Wolfgang Küchlin and
Carsten Sinz Proving Consistency Assertions for
Automotive Product Data Management . . . 145--163
Fabio Massacci and
Laura Marraro Logical Cryptanalysis as a SAT Problem 165--203
Patrick Mills and
Edward Tsang Guided Local Search for Solving SAT and
Weighted MAX--SAT Problems . . . . . . . 205--223
Irina Rish and
Rina Dechter Resolution versus Search: Two Strategies
for SAT . . . . . . . . . . . . . . . . 225--275
Hantao Zhang and
Mark Stickel Implementing the Davis--Putnam Method 277--296
Peter Balsiger and
Alain Heuerding and
Stefan Schwendimann A Benchmark Method for the Propositional
Modal Logics K, KT, S4 . . . . . . . . . 297--317
Fabio Massacci Single Step Tableaux for Modal Logics 319--364
R. Padmanabhan and
P. Penner A Hyperbase for Binary Lattice
Hyperidentities . . . . . . . . . . . . 365--370
Geoff Sutcliffe The CADE-16 ATP System Competition . . . 371--396
Edward A. Hirsch New Worst-Case Upper Bounds for SAT . . 397--420
Holger H. Hoos and
Thomas Stützle Local Search Algorithms for SAT: An
Empirical Evaluation . . . . . . . . . . 421--481
E. Thomas Richards and
Barry Richards Nonsystematic Search and No-Good
Learning . . . . . . . . . . . . . . . . 483--533
Bruce Spencer and
J. D. Horton Efficient Algorithms to Detect and
Restore Minimality, an Extension of the
Regular Restriction of Resolution . . . 1--34
François Bry and
Adnan Yahya Positive Unit Hyperresolution Tableaux
and Their Application to Minimal Model
Generation . . . . . . . . . . . . . . . 35--82
Hongbo Li Vectorial Equations Solving for
Mechanical Geometry Theorem Proving . . 83--121
Dieter Hutter and
Michael Kohlhase Managing Structural Information by
Higher-Order Colored Unification . . . . 123--164
Anonymous Erratum . . . . . . . . . . . . . . . . 165--165
David A. Plaisted and
Yunshan Zhu Ordered Semantic Hyper-Linking . . . . . 167--217
Shang-Ching Chou and
Xiao-Shan Gao and
Jing-Zhong Zhang A Deductive Database Approach to
Automated Geometry Theorem Proving and
Discovering . . . . . . . . . . . . . . 219--246
Marek A. Suchenek Evaluation of Queries under Closed-World
Assumption. Part II: The Hierarchical
Case . . . . . . . . . . . . . . . . . . 247--289
A. Prasad Sistla and
Clement Yu Reasoning about Qualitative Spatial
Relationships . . . . . . . . . . . . . 291--328
Anonymous Author Index to Volume 25 . . . . . . . 329--329
Anonymous Subject Index to Volume 25 . . . . . . . 331--332
Anonymous Contents to Volume 25 . . . . . . . . . 333--334
Jürgen Giesl Induction Proofs with Partial Functions 1--49
Tobias Nipkow More Church--Rosser Proofs . . . . . . . 51--66
Chih-Hung Wu and
Shie-Jue Lee Parallelization of a Hyper-Linking-Based
Theorem Prover . . . . . . . . . . . . . 67--106
Laurent Théry A Machine-Checked Implementation of
Buchberger's Algorithm . . . . . . . . . 107--137
Wolfgang Gehrke and
Jochen Pfalzgraf Computer-Aided Construction of Finite
Geometric Spaces: Automated Verification
of Geometric Constraints . . . . . . . . 139--160
Matt Kaufmann and
J. Strother Moore Structured Theory Development for a
Mechanized Logic . . . . . . . . . . . . 161--203
Ulrich Berger and
Helmut Schwichtenberg and
Monika Seisenberger The Warshall Algorithm and Dickson's
Lemma: Two Examples of Realistic Program
Extraction . . . . . . . . . . . . . . . 205--221
Jürgen Avenhaus and
David A. Plaisted General Algorithms for Permutations in
Equational Inference . . . . . . . . . . 223--268
William M. Farmer STMM: A Set Theory for Mechanized
Mathematics . . . . . . . . . . . . . . 269--289
F. Giunchiglia and
P. Pecchiari and
C. Talcott Reasoning Theories . . . . . . . . . . . 291--331
C. A. Johnson On the Computation of the Disjunctive
Well-Founded Semantics . . . . . . . . . 333--356
M. Randall Holmes and
Jim Alves-Foss The Watson Theorem Prover . . . . . . . 357--408
Robert McNaughton Semi-Thue Systems with an Inhibitor . . 409--431
Anonymous Author Index to Volume 26 . . . . . . . 433--433
Anonymous Subject Index to Volume 26 . . . . . . . 435--435
Anonymous Contents to Volume 26 . . . . . . . . . 437--438
David Basin and
Amy Felty Current Trends in Logical Frameworks and
Metalanguages . . . . . . . . . . . . . 1--2
Paul Callaghan and
Zhaohui Luo An Implementation of LF with Coercive
Subtyping & Universes . . . . . . . . . . 3--27
Mirna Bognar and
Roel de Vrijer A Calculus of Lambda Calculus Contexts 29--59
Paula Severi and
Nora Szasz Studies of a Theory of Specifications
with Built-in Program Extraction . . . . 61--87
Larry Wos A Milestone Reached and a Secret
Revealed . . . . . . . . . . . . . . . . 89--95
Dolph Ulrich A Legacy Recalled and a Tradition
Continued . . . . . . . . . . . . . . . 97--122
Robert Veroff Finding Shortest Proofs: An Application
of Linked Inference Rules . . . . . . . 123--139
Kenneth Harris and
Branden Fitelson Distributivity in $ {\L } \aleph_0 $ and
Other Sentential Logics . . . . . . . . 141--156
Robert Veroff Solving Open Questions and Other
Challenge Problems Using Proof Sketches 157--174
Larry Wos Conquering the Meredith Single Axiom . . 175--199
Branden Fitelson and
Larry Wos Missing Proofs Found . . . . . . . . . . 201--225
G. Sutcliffe The CADE-17 ATP System Competition . . . 227--250
Michael L. Littman and
Stephen M. Majercik and
Toniann Pitassi Stochastic Boolean Satisfiability . . . 251--296
Guido Fiorino An $ O(n \log n)$-SPACE Decision
Procedure for the Propositional Dummett
Logic . . . . . . . . . . . . . . . . . 297--311
Lifeng He I-SATCHMO: An Improvement of SATCHMO . . 313--322
Ruben A. Gamboa and
Matt Kaufmann Nonstandard Analysis in ACL2 . . . . . . 323--351
Guilherme Bittencourt and
Isabel Tonin An Algorithm for Dual Transformation in
First-Order Logic . . . . . . . . . . . 353--389
P. A. Bonatti Resolution for Skeptical Stable Model
Semantics . . . . . . . . . . . . . . . 391--421
Anonymous Author Index to Volume 27 . . . . . . . 423--423
Anonymous Subject Index to Volume 27 . . . . . . . 425--425
Anonymous Contents to Volume 27 . . . . . . . . . 427--428
Adnan H. Yahya Duality for Goal-Driven Query Processing
in Disjunctive Deductive Databases . . . 1--34
Steven Eker Single Elementary
Associative--Commutative Matching . . . 35--51
Yi-Dong Shen and
Li-Yan Yuan and
Jia-Huai You SLT-Resolution for the Well-Founded
Semantics . . . . . . . . . . . . . . . 53--97
Ian P. Gent and
Toby Walsh Satisfiability in the Year 2000 . . . . 99--99
Marco Cadoli and
Marco Schaerf and
Andrea Giovanardi and
Massimo Giovanardi An Algorithm to Evaluate Quantified
Boolean Formulae and Its Experimental
Evaluation . . . . . . . . . . . . . . . 101--142
Enrico Giunchiglia and
Armando Tacchella and
Fausto Giunchiglia SAT-Based Decision Procedures for
Classical Modal Logics . . . . . . . . . 143--171
Ian Horrocks and
Peter F. Patel-Schneider Evaluating Optimized Decision Procedures
for Propositional Modal $ K_{(m)} $
Satisfiability . . . . . . . . . . . . . 173--204
Ullrich Hustadt and
Renate A. Schmidt Using Resolution for Testing Modal
Satisfiability and Building Models . . . 205--232
Anonymous Erratum . . . . . . . . . . . . . . . . 233--233
Robert Cremanns and
Friedrich Otto A Completion Procedure for Finitely
Presented Groups That Is Based on Word
Cycles . . . . . . . . . . . . . . . . . 235--256
Predrag Jani\vci\'c and
Alan Bundy A General Setting for Flexibly Combining
and Augmenting Decision Procedures . . . 257--305
G. Sutcliffe and
C. B. Suttner and
F. J. Pelletier The IJCAR ATP System Competition . . . . 307--320
Henk Barendregt and
Erik Barendsen Autarkic Computations in Formal Proofs 321--336
Teodor Knapik Checking Simple Properties of Transition
Systems Defined by Thue Specifications 337--369
J. N. Hooker and
G. Rago and
V. Chandru and
A. Shrivastava Partial Instantiation Methods for
Inference in First-Order Logic . . . . . 371--396
Angelo Montanari and
Alberto Policriti and
Matteo Slanina Alternative Translation Techniques for
Propositional and First-Order Modal
Logics . . . . . . . . . . . . . . . . . 397--415
Eugene Goldberg Proving Unsatisfiability of CNFs Locally 417--434
Anonymous Author Index to Volume 28 . . . . . . . 435--435
Anonymous Subject Index to Volume 28 . . . . . . . 437--437
Anonymous Contents to Volume 28 . . . . . . . . . 439--440
William McCune and
Robert Veroff and
Branden Fitelson and
Kenneth Harris and
Andrew Feist and
Larry Wos Short Single Axioms for Boolean Algebra 1--16
Adnan Yahya and
David A. Plaisted Ordered Semantic Hyper Tableaux . . . . 17--57
John Slaney More Proofs of an Axiom of \Lukasiewicz 59--66
Ruediger Thiele and
Larry Wos Hilbert's Twenty-Fourth Problem . . . . 67--89
Vivek S. Borkar and
Vijay Chandru and
Sanjoy K. Mitter Mathematical Programming Embeddings of
Logic . . . . . . . . . . . . . . . . . 91--106
Larry Wos and
Dolph Ulrich and
Branden Fitelson Vanquishing the XCB Question: The
Methodological Discovery of the Last
Shortest Single Axiom for the
Equivalential Calculus . . . . . . . . . 107--124
Leila Amgoud and
Claudette Cayrol Inferring from Inconsistency in
Preference-Based Argumentation
Frameworks . . . . . . . . . . . . . . . 125--169
G. Mashevitzky Unification Types of Completely Regular
Semigroups . . . . . . . . . . . . . . . 171--182
Fairouz Kamareddine Preface: Mechanizing and Automating
Mathematics: In honour of N. G. de
Bruijn . . . . . . . . . . . . . . . . . 183--188
Grzegorz Bancerek and
Piotr Rudnicki A Compendium of Continuous Lattices in
MIZAR . . . . . . . . . . . . . . . . . 189--224
Yves Bertot and
Nicolas Magaud and
Paul Zimmermann A Proof of GMP Square Root . . . . . . . 225--252
Marc Bezem and
Dimitri Hendriks and
Hans de Nivelle Automated Proof Construction in Type
Theory Using Resolution . . . . . . . . 253--275
Dimitri Hendriks Proof Reflection in Coq . . . . . . . . 277--307
Quang Huy Nguyen and
Claude Kirchner and
Hél\`ene Kirchner External Rewriting for Skeptical Proof
Assistants . . . . . . . . . . . . . . . 309--336
Virgile Prevosto and
Damien Doligez Algorithms and Proofs Inheritance in the
FOC Language . . . . . . . . . . . . . . 337--363
Freek Wiedijk A New Implementation of Automath . . . . 365--387
Markus Wenzel and
Freek Wiedijk A Comparison of Mizar and Isar . . . . . 389--411
Anonymous Author Index to Volume 29 . . . . . . . 413--413
Anonymous Subject Index to Volume 29 . . . . . . . 415--415
Anonymous Contents to Volume 29 . . . . . . . . . 417--418
Cesare Tinelli Cooperation of Background Reasoners in
Theory Reasoning by Residue Sharing . . 1--31
Antonella Santone and
Gigliola Vaglini Modifying LOTOS Specifications by Means
of Automatable Formula-Based
Integrations . . . . . . . . . . . . . . 33--58
Fairouz Kamareddine and
Haiyan Qiao Formalizing Strong Normalization Proofs
of Explicit Substitution Calculi in ALF 59--98
Miquel Bofill and
Guillem Godoy and
Robert Nieuwenhuis and
Albert Rubio Paramodulation and Knuth--Bendix
Completion with Nontotal and
Nonmonotonic Orderings . . . . . . . . . 99--120
Andrei Voronkov Proof-Search in Intuitionistic Logic
with Equality, or Back to Simultaneous
Rigid $E$-Unification . . . . . . . . . 121--151
Michaël Rusinowitch and
Sorin Stratulat and
Francis Klay Mechanical Verification of an Ideal
Incremental ABR Conformance Algorithm 153--177
Larry Wos The Strategy of Cramming . . . . . . . . 179--204
Krishnendu Chatterjee and
Pallab Dasgupta and
P. P. Chakrabarti A Branching Time Temporal Framework for
Quantitative Reasoning . . . . . . . . . 205--232
Tobias Nipkow Java Bytecode Verification . . . . . . . 233--233
Xavier Leroy Java Bytecode Verification: Algorithms
and Formalizations . . . . . . . . . . . 235--269
Stephen N. Freund and
John C. Mitchell A Type System for the Java Bytecode
Language and Verifier . . . . . . . . . 271--321
Robert F. Stärk and
Joachim Schmid Completeness of a Bytecode Verifier and
a Certifying Java-to-JVM Compiler . . . 323--361
G. Klein and
M. Wildmoser Verified Bytecode Subroutines . . . . . 363--398
David A. Basin and
Stefan Friedrich and
Marek Gawkowski Bytecode Verification by Model Checking 399--444
Anonymous Author Index to Volume 30 . . . . . . . 445--445
Anonymous Subject Index to Volume 30 . . . . . . . 447--447
Anonymous Contents to Volume 30 . . . . . . . . . 449--450
Robert Veroff A Shortest $2$-Basis for Boolean Algebra
in Terms of the Sheffer Stroke . . . . . 1--9
Lin Hai and
Sun Jigui and
Zhang Yimin Theorem Proving Based on the Extension
Rule . . . . . . . . . . . . . . . . . . 11--21
G. Sutcliffe and
C. B. Suttner The CADE-18 ATP System Competition . . . 23--32
Gilles Dowek and
Thér\`ese Hardin and
Claude Kirchner Theorem Proving Modulo . . . . . . . . . 33--72
R. Gentilini and
C. Piazza and
A. Policriti From Bisimulation to Simulation:
Coarsest Partition Problems . . . . . . 73--103
Deepak Kapur Announcement . . . . . . . . . . . . . . 105--105
Panagiotis Manolios and
J. Strother Moore Partial Functions in ACL2 . . . . . . . 107--127
Leo Bachmair and
Ashish Tiwari and
Laurent Vigneron Abstract Congruence Closure . . . . . . 129--168
Peter B. Andrews Herbrand Award Acceptance Speech . . . . 169--187
Amy P. Felty Preface . . . . . . . . . . . . . . . . 189--190
Nadeem A. Hamid and
Zhong Shao and
Valery Trifonov and
Stefan Monnier and
Zhaozhong Ni A Syntactic Approach to Foundational
Proof-Carrying Code . . . . . . . . . . 191--229
Andrew W. Appel and
Neophytos Michael and
Aaron Stump and
Roberto Virga A Trustworthy Proof Checker . . . . . . 231--260
David Aspinall and
Adriana Compagnoni Heap-Bounded Assembly Language . . . . . 261--302
Eva Rose Lightweight Bytecode Verification . . . 303--334
James Riely and
Matthew Hennessy Trust and Partial Typing in Open Systems
of Mobile Agents . . . . . . . . . . . . 335--370
Anonymous Author Index to Volume 31 . . . . . . . 371--371
Anonymous Subject Index to Volume 31 . . . . . . . 373--373
Anonymous Contents to Volume 31 . . . . . . . . . 375--376
Deepak Kapur Preface . . . . . . . . . . . . . . . . 1--2
Noboru Matsuda and
Kurt VanLehn GRAMY: A Geometry Theorem Prover Capable
of Construction . . . . . . . . . . . . 3--33
Christoph Walther and
Stephan Schweitzer Verification in the Classroom . . . . . 35--73
Peter B. Andrews and
Chad E. Brown and
Frank Pfenning and
Matthew Bishop and
Sunil Issar and
Hongwei Xi ETPS: A System to Help Students Write
Formal Proofs . . . . . . . . . . . . . 75--92
Lin Hai and
Sun Jigui Knowledge Compilation Using the
Extension Rule . . . . . . . . . . . . . 93--102
Harald Ganzinger and
Robert Nieuwenhuis and
Pilar Nivela Fast Term Indexing with Coded Context
Trees . . . . . . . . . . . . . . . . . 103--120
Christoph Kreitz and
Heiko Mantel A Matrix Characterization for
Multiplicative Exponential Linear Logic 121--166
C. A. Johnson Top-Down Query Processing in First-Order
Deductive Databases under the DWFS . . . 167--184
Deepak Kapur Preface . . . . . . . . . . . . . . . . 185--186
Maxim Makatchev and
Pamela W. Jordan and
Kurt VanLehn Abductive Theorem Proving for Analyzing
Student Explanations to Guide Feedback
in Intelligent Tutoring Systems . . . . 187--226
Richard Sommer and
Gregory Nuckols A Proof Environment for Teaching
Mathematics . . . . . . . . . . . . . . 227--258
P. Baumgartner and
U. Furbach and
M. Gross-Hardt and
A. Sinner Living Book-- Deduction, Slicing, and
Interaction . . . . . . . . . . . . . . 259--286
Deepak Kapur Obituary . . . . . . . . . . . . . . . . ??
Francisco-Jesús Martín-Mateos and
José-Antonio Alonso and
María-José Hidalgo and
José-Luis Ruiz-Reina Formal verification of a generic
framework to synthesize SAT-provers . . ??
Xavier Urbain Modular and Incremental Automated
Termination Proofs . . . . . . . . . . . ??
Siva Anantharaman and
Paliath Narendran and
Michael Rusinowitch Unification Modulo ACUI Plus
Distributivity Axioms . . . . . . . . . 1--28
Lawrence C. Paulson Organizing Numerical Theories Using
Axiomatic Type Classes . . . . . . . . . 29--49
Jürgen Zimmer and
Erica Melis Constraint Solving for Proof Planning 51--88
Chuck Liang and
Gopalan Nadathur and
Xiaochu Qi Choices in Representation and Reduction
Strategies for Lambda Terms in
Intensional Contexts . . . . . . . . . . 89--132
N. Peltier Representing and Building Models for
Decidable Subclasses of Equational
Clausal Logic . . . . . . . . . . . . . 133--170
Monty Newborn and
Zongyan Wang Octopus: Combining Learning and Parallel
Search . . . . . . . . . . . . . . . . . 171--218
Deepak Kapur and
Laurent Vigneron Preface . . . . . . . . . . . . . . . . 219--220
Silvio Ghilardi Model-Theoretic Methods in Combined
Constraint Satisfiability . . . . . . . 221--249
Calogero G. Zarba and
Domenico Cantone and
Jacob T. Schwartz A Decision Procedure for a Sublanguage
of Set Theory Involving Monotone,
Additive, and Multiplicative Functions,
I: The Two-Level Case . . . . . . . . . 251--269
Thierry Boy de la Tour and
Mnacho Echenim On the Complexity of Deduction Modulo
Leaf Permutative Equations . . . . . . . 271--317
Josef Urban MPTP --- Motivation, Implementation,
First Experiments . . . . . . . . . . . 319--339
Guillaume Feuillade and
Thomas Genet and
Valérie Viet Triem Tong Reachability Analysis over Term
Rewriting Systems . . . . . . . . . . . 341--383
Calogero G. Zarba Combining Sets with Cardinals . . . . . 1--29
Anja Remshagen and
Klaus Truemper An Effective Algorithm for the Futile
Questioning Problem . . . . . . . . . . 31--47
Domenico Cantone and
Calogero G. Zarba and
Rosa Ruggeri Cannata A Tableau-Based Decision Procedure for a
Fragment of Set Theory with Iterated
Membership . . . . . . . . . . . . . . . 49--72
Bernard Jurkowiak and
Chu Min Li and
Gil Utard A Parallelization Scheme Based on Work
Stealing for a Class of SAT Solvers . . 73--101
Jürgen Giesl and
Deepak Kapur Preface . . . . . . . . . . . . . . . . 103--104
H. Zantema Termination of String Rewriting Proved
Automatically . . . . . . . . . . . . . 105--139
Alexander Serebrenik and
Danny De Schreye Termination of Floating-Point
Computations . . . . . . . . . . . . . . 141--177
Brigitte Pientka Verifying Termination and Reduction
Properties about Higher-Order Logic
Programs . . . . . . . . . . . . . . . . 179--207
Cesare Tinelli and
Calogero G. Zarba Combining Nonstably Infinite Theories 209--238
Konstantine Arkoudas Simplifying Proofs in Fitch-Style
Natural Deduction Systems . . . . . . . 239--294
M. C. Fernández-Gago and
U. Hustadt and
C. Dixon and
M. Fisher and
B. Konev First-Order Temporal Verification in
Practice . . . . . . . . . . . . . . . . 295--321
Jügen Giesl and
Deepak Kapur Preface . . . . . . . . . . . . . . . . 323--323
Alfons Geser and
Dieter Hofbauer and
Johannes Waldmann Termination Proofs for String Rewriting
Systems via Inverse Match-Bounds . . . . 365--385
Panagiotis Manolios and
Daron Vroon Ordinal Arithmetic: Algorithms and
Mechanization . . . . . . . . . . . . . 387--423
Evelyne Contejean and
Claude Marché and
Ana Paula Tomás and
Xavier Urbain Mechanically Proving Termination Using
Polynomial Interpretations . . . . . . . ??
Enrico Giunchiglia and
Toby Walsh Satisfiability in the Year 2005 . . . . 1--2
Ateet Bhalla and
Inês Lynce and
José T. de Sousa and
João Marques-Silva Heuristic-Based Backtracking Relaxation
for Propositional Satisfiability . . . . 3--24
Guoqiang Pan and
Moshe Y. Vardi Symbolic Techniques in Satisfiability
Solving . . . . . . . . . . . . . . . . 25--50
Michael Alekhnovich and
Edward A. Hirsch and
Dmitry Itsykson Exponential Lower Bounds for the Running
Time of DPLL Algorithms on Satisfiable
Formulas . . . . . . . . . . . . . . . . 51--72
Stefan Szeider Backdoor Sets for DLL Subsolvers . . . . 73--88
Jan Johannsen The Complexity of Pure Literal
Elimination . . . . . . . . . . . . . . 89--95
John Thornton Clause Weighting Local Search for SAT 97--142
Alan M. Frisch and
Timothy J. Peugniez and
Anthony J. Doggett and
Peter W. Nightingale Solving Non--Boolean Satisfiability
Problems with Stochastic Local Search: A
Comparison of Encodings . . . . . . . . 143--179
Yacine Boufkhad and
Olivier Dubois and
Yannet Interian and
Bart Selman Regular Random $k$-SAT: Properties of
Balanced Formulas . . . . . . . . . . . 181--200
Andreas Meier and
Volker Sorge Applying SAT Solving in Classification
of Finite Algebras . . . . . . . . . . . 201--235
Alessandro Armando and
Claudio Castellini and
Enrico Giunchiglia and
Marco Maratea The SAT-based Approach to Separation
Logic . . . . . . . . . . . . . . . . . 237--263
Marco Bozzano and
Roberto Bruttomesso and
Alessandro Cimatti and
Tommi Junttila and
Peter van Rossum and
Stephan Schulz and
Roberto Sebastiani M ath SAT: Tight Integration of SAT and
Mathematical Decision Procedures . . . . 265--293
Gilles Barthe and
Pierre Courtieu and
Guillaume Dufay and
Simão Melo de Sousa Tool-Assisted Specification and
Verification of Typed Low--Level
Languages . . . . . . . . . . . . . . . 295--354
Robert S. Boyer and
Wilfred J. Legato and
Victor W. Marek Toward Automating the Discovery of
Decreasing Measures . . . . . . . . . . 355--371
Clark Barrett and
Leonardo de Moura and
Aaron Stump Design and Results of the First
Satisfiability Modulo Theories
Competition (SMT-COMP 2005) . . . . . . 373--390
N. Peltier Some Techniques for Proving Termination
of the Hyperresolution Calculus . . . . 391--427
Nimish Shah Book Review: \booktitleRippling:
Meta-Level Guidance for Mathematical
Reasoning, by Alan Bundy, David Basin,
Dieter Hutter, and Andrew Ireland,
Cambridge University Press, 2005 . . . . 429--431
Alessandro Armando and
David Basin and
Jorge Cuellar Automated Reasoning for Security
Protocol Analysis . . . . . . . . . . . 1--3
Giampaolo Bella and
Fabio Massacci and
Lawrence C. Paulson Verifying the SET Purchase Protocols . . 5--37
Rohit Chadha and
Steve Kremer and
Andre Scedrov Formal Analysis of Multiparty Contract
Signing . . . . . . . . . . . . . . . . 39--83
Stéphanie Delaune and
Florent Jacquemard Decision Procedures for the Security of
Protocols with Probabilistic Encryption
against Offline Dictionary Attacks . . . 85--124
Hans Hüttel and
Ji\vrí Srba Decidability Issues for Extended
Ping--Pong Protocols . . . . . . . . . . 125--147
Graham Steel and
Alan Bundy Attacking Group Protocols by Refuting
Incorrect Inductive Conjectures . . . . 149--176
Gilles Audemard and
Bela\"\id Benhamou and
Laurent Henocque Predicting and Detecting Symmetries in
FOL Finite Model Search . . . . . . . . 177--212
Viktor Kuncak and
Huu Hai Nguyen and
Martin Rinard Deciding Boolean Algebra with Presburger
Arithmetic . . . . . . . . . . . . . . . 213--239
Nick C. Fiala and
Keith M. Agre Searching for Shortest Single Axioms for
Groups of Exponent 6 . . . . . . . . . . 241--257
Carlos Simpson Explaining Gabriel--Zisman Localization
to the Computer . . . . . . . . . . . . 259--285
Bernd Fischer and
Geoff Sutcliffe and
Stephan Schulz Empirically Successful Automated
Reasoning: Systems Issue . . . . . . . . 287--287
Bernd Löchner Things to Know when Implementing KBO . . 289--310
Michael Beeson Mathematical Induction in Otter--Lambda 311--344
Andrew Ireland and
Bill J. Ellis and
Andrew Cook and
Roderick Chapman and
Janet Barnes An Integrated Approach to High Integrity
Software Verification . . . . . . . . . 379--410
Enrico Giunchiglia and
Yuliya Lierler and
Marco Maratea Answer Set Programming Based on
Propositional Satisfiability . . . . . . ??
Bernd Fischer and
Geoff Sutcliffe and
Stephan Schulz Empirically Successful Automated
Reasoning: Applications Issue . . . . . 1--1
R. Veroff and
M. Spinks Axiomatizing the Skew Boolean
Propositional Calculus . . . . . . . . . 3--20
Josef Urban MPTP 0.2: Design, Implementation, and
Initial Experiments . . . . . . . . . . 21--43
Carsten Sinz and
Wolfgang Küchlin and
Dieter Feichtinger Checking Consistency and Completeness of
On-Line Product Manuals . . . . . . . . 45--66
José-Luis Ruiz-Reina and
Francisco-Jesús Martín-Mateos and
José-Antonio Alonso and
María-José Hidalgo Formal Correctness of a Quadratic
Unification Algorithm . . . . . . . . . 67--92
Panagiotis Manolios and
Sudarshan K. Srinivasan A Framework for Verifying Bit-Level
Pipelined Machines Based on Automated
Deduction and Decision Procedures . . . 93--116
Oliver Pell Verification of FPGA Layout Generators
in Higher-Order Logic . . . . . . . . . 117--152
Jürgen Giesl and
Deepak Kapur Third Special Issue on Techniques for
Automated Termination Proofs . . . . . . 153--154
Jürgen Giesl and
René Thiemann and
Peter Schneider-Kamp and
Stephan Falke Mechanizing and Improving Dependency
Pairs . . . . . . . . . . . . . . . . . 155--203
Kusakari Keiichirou and
Nakamura Masaki and
Toyama Yoshihito Elimination Transformations for
Associative--Commutative Rewriting
Systems . . . . . . . . . . . . . . . . 205--229
Olivier Bailleux and
Pierre Marquis Some Computational Aspects of
distance-sat . . . . . . . . . . . . . . 231--260
Gilles Dequen and
Olivier Dubois An Efficient Approach to Solving Random
$k$-SAT Problems . . . . . . . . . . . . 261--276
Steven Givant The Calculus of Relations as a
Foundation for Mathematics . . . . . . . 277--322
Sébastien Limet and
Gernot Salzer Tree Tuple Languages from the Logic
Programming Point of View . . . . . . . 323--349
Bernhard Beckert and
Lawrence C. Paulson Preface . . . . . . . . . . . . . . . . 1--2
Roger Antonsen and
Arild Waaler Liberalized Variable Splitting . . . . . 3--30
Domenico Cantone and
Marianna Nicolosi-Asmundo A Sound Framework for $ \delta $-Rule
Variants in Free-Variable Semantic
Tableaux . . . . . . . . . . . . . . . . 31--56
Swen Jacobs and
Uwe Waldmann Comparing Instance Generation Methods
for Automated Reasoning . . . . . . . . 57--78
Reinhold Letz and
Gernot Stenz The Disconnection Tableau Calculus . . . 79--126
Martin Giese Superposition-based Equality Handling
for Analytic Tableaux . . . . . . . . . 127--153
Neil V. Murray and
Erik Rosenthal Efficient Query Processing with Reduced
Implicate Tries . . . . . . . . . . . . 155--172
Davide Bresolin and
Angelo Montanari and
Guido Sciavicco An Optimal Decision Procedure for Right
Propositional Neighborhood Logic . . . . 173--199
Dominique Larchey-Wendling Graph-based Decision for Gödel--Dummett
Logics . . . . . . . . . . . . . . . . . 201--225
Carsten Lutz and
Maja Mili\vci\'c A Tableau Algorithm for Description
Logics with Concrete Domains and General
TBoxes . . . . . . . . . . . . . . . . . 227--259
Thomas Raths and
Jens Otten and
Christoph Kreitz The ILTP Problem Library for
Intuitionistic Logic . . . . . . . . . . 261--271
R. Gamboa and
J. Cowles Theory Extension in ACL2(r) . . . . . . 273--301
Marc Aiguier and
Diane Bahrami Structures for Abstract Rewriting . . . 303--351
Jeremy Avigad and
Kevin Donnelly A Decision Procedure for Linear ``Big
O'' Equations . . . . . . . . . . . . . 353--373
Alberto Ciaffaglione and
Luigi Liquori and
Marino Miculan Reasoning about Object-based Calculi in
(Co)Inductive Type Theory and the Theory
of Contexts . . . . . . . . . . . . . . 1--47
Hans Kleine Büning and
K. Subramani and
Xishun Zhao Boolean Functions as Models for
Quantified Boolean Formulas . . . . . . 49--75
Barbara Morawska General $E$-unification with Eager
Variable Elimination and a Nice Cycle
Rule . . . . . . . . . . . . . . . . . . 77--106
David Aspinall and
Christoph Lüth Special Issue on User Interfaces in
Theorem Proving: Preface . . . . . . . . 107--108
Andrea Asperti and
Claudio Sacerdoti Coen and
Enrico Tassi and
Stefano Zacchiroli User Interaction with the Matita Proof
Assistant . . . . . . . . . . . . . . . 109--139
Paul Cairns and
Jeremy Gow Integrating Searching and Authoring in
Mizar . . . . . . . . . . . . . . . . . 141--160
Julien Narboux A Graphical User Interface for Formal
Proofs in Geometry . . . . . . . . . . . 161--180
William Billingsley and
Peter Robinson Student Proof Exercises Using MathsTiles
and Isabelle/HOL in an Intelligent Book 181--218
Carsten Sinz Visualizing SAT Instances and Runs of
the DPLL Algorithm . . . . . . . . . . . 219--243
Franz Baader Preface to Special Issue on Reasoning in
Description Logics . . . . . . . . . . . 245--247
Ian Horrocks and
Ulrike Sattler A Tableau Decision Procedure for $
\mathcal {SHOIQ} $ . . . . . . . . . . . 249--276
Dmitry Tsarkov and
Ian Horrocks and
Peter F. Patel-Schneider Optimizing Terminological Reasoning for
Expressive Description Logics . . . . . 277--316
Stefan Schlobach and
Zhisheng Huang and
Ronald Cornet and
Frank van Harmelen Debugging Incoherent Terminologies . . . 317--349
Ullrich Hustadt and
Boris Motik and
Ulrike Sattler Reasoning in Description Logics by a
Reduction to Disjunctive Datalog . . . . 351--384
Diego Calvanese and
Giuseppe De Giacomo and
Domenico Lembo and
Maurizio Lenzerini and
Riccardo Rosati Tractable Reasoning and Efficient Query
Answering in Description Logics: The
DL--Lite Family . . . . . . . . . . . . 385--429
Gem Stapleton and
Judith Masthoff and
Jean Flower and
Andrew Fish and
Jane Southern Automated Theorem Proving in Euler
Diagram Systems . . . . . . . . . . . . 431--470
Julien Forest and
Delia Kesner Expression Reduction Systems with
Patterns . . . . . . . . . . . . . . . . 513--541
Daniel R. Brooks and
Esra Erdem and
Selim T. Erdo\ugan and
James W. Minett and
Don Ringe Inferring Phylogenetic Trees Using
Answer Set Programming . . . . . . . . . ??
Mark H. Liffiton and
Karem A. Sakallah Algorithms for Computing Minimal
Unsatisfiable Subsets of Constraints . . 1--33
Jia Meng and
Lawrence C. Paulson Translating Higher-Order Clauses to
First-Order Clauses . . . . . . . . . . 35--60
Marc Bezem and
Dimitri Hendriks On the Mechanization of the Proof of
Hessenberg's Theorem in Coherent Logic 61--85
Ulrich Furbach IJCAR Preface . . . . . . . . . . . . . 87--88
Yevgeny Kazakov and
Boris Motik A Resolution-Based Decision Procedure
for $ \boldsymbol \mathcal {SHOIQ} $ . . 89--116
David Toman and
Grant Weddell On Keys and Functional Dependencies as
First-Class Citizens in Description
Logics . . . . . . . . . . . . . . . . . 117--132
Kaustuv Chaudhuri and
Frank Pfenning and
Greg Price A Logical Characterization of Forward
and Backward Chaining in the Inverse
Method . . . . . . . . . . . . . . . . . 133--177
Andrei Paskevich Connection Tableaux with Lazy
Paramodulation . . . . . . . . . . . . . 179--194
Jörg Endrullis and
Johannes Waldmann and
Hans Zantema Matrix Interpretations for Proving
Termination of Term Rewriting . . . . . 195--220
Volker Sorge and
Andreas Meier and
Roy McCasland and
Simon Colton Automatic Construction and Verification
of Isotopy Invariants . . . . . . . . . 221--243
Sandip Ray and
Warren A. Hunt, Jr.. and
John Matthews and
J. Strother Moore A Mechanical Analysis of Program
Verification Strategies . . . . . . . . 245--269
Jesús Aransay and
Clemens Ballarin and
Julio Rubio A Mechanized Proof of the Basic
Perturbation Lemma . . . . . . . . . . . 271--292
Bishop Brock and
Matt Kaufmann and
J. Strother Moore Rewriting with Equivalence Relations in
ACL2 . . . . . . . . . . . . . . . . . . 293--306
Laurence Rideau and
Bernard Paul Serpette and
Xavier Leroy Tilting at Windmills with Coq: Formal
Verification of a Compilation Algorithm
for Parallel Moves . . . . . . . . . . . 307--326
Christian Urban Nominal Techniques in Isabelle/HOL . . . 327--356
Yevgeny Kazakov and
Boris Motik A Resolution-Based Decision Procedure
for $ \boldsymbol \mathcal {SHOIQ} $ . . 357--357
Xavier Leroy and
Sandrine Blazy Formal Verification of a C-like Memory
Model and Its Uses for Verifying Program
Transformations . . . . . . . . . . . . 1--31
Magdalena Ortiz and
Diego Calvanese and
Thomas Eiter Data Complexity of Query Answering in
Expressive Description Logics via
Tableaux . . . . . . . . . . . . . . . . 61--98
Amine Chaieb and
Tobias Nipkow Proof Synthesis and Reflection for
Linear Arithmetic . . . . . . . . . . . ??
Volker Haarslev and
Ralf Möller On the Scalability of Description Logic
Instance Retrieval . . . . . . . . . . . 99--142
André Platzer Differential Dynamic Logic for Hybrid
Systems . . . . . . . . . . . . . . . . 143--189
Serge Autexier and
Heiko Mantel and
Stephan Merz and
Tobias Nipkow Preface . . . . . . . . . . . . . . . . 191--192
Hasan Amjad Data Compression for Proof Replay . . . 193--218
Achim D. Brucker and
Burkhart Wolff An Extensible Encoding of
Object-oriented Data Models in HOL . . . 219--249
Osman Hasan and
Sofi\`ene Tahar Using Theorem Proving to Verify
Expectation and Variance for Discrete
Random Variables . . . . . . . . . . . . 295--323
Roberto Gorrieri and
Fabio Martinelli and
Marinella Petrocchi Formal Models and Analysis of Secure
Multicast in Wired and Wireless Networks 325--364
Nick Moffat and
Michael Goldsmith Assumption--Commitment Support for CSP
Model Checking . . . . . . . . . . . . . 365--398
Alastair F. Donaldson and
Alice Miller Automatic Symmetry Detection for Promela ??
Osman Hasan and
Sofi\`ene Tahar Performance Analysis and Functional
Verification of the Stop-and-Wait
Protocol in HOL . . . . . . . . . . . . 1--33
C. A. Johnson Computing Only Minimal Answers in
Disjunctive Deductive Databases . . . . 35--76
Marko Samer and
Stefan Szeider Backdoor Sets of Quantified Boolean
Formulas . . . . . . . . . . . . . . . . 77--97
Magnus Björk First Order Stålmarck . . . . . . . . . . 99--122
Gerwin Klein and
Ralf Huuck and
Bastian Schlich Operating System Verification . . . . . 123--124
Harvey Tuch Formal Verification of C Systems Code 125--187
Hendrik Tews and
Marcus Völp and
Tjark Weber Formal Memory Models for the
Verification of Low-Level
Operating-System Code . . . . . . . . . 189--227
María del Mar Gallardo and
Pedro Merino and
David Sanán Model Checking Dynamic Memory Allocation
in Operating Systems . . . . . . . . . . 229--264
Syrine Tlili and
Mourad Debbabi Interprocedural and Flow-Sensitive Type
Analysis for Memory and Type Safety of C
Code . . . . . . . . . . . . . . . . . . 265--300
Xinyu Feng and
Zhong Shao and
Yu Guo and
Yuan Dong Certifying Low-Level Programs with
Hardware Interrupts and Preemptive
Threads . . . . . . . . . . . . . . . . 301--347
Matthias Daum and
Jan Dörrenbächer and
Burkhart Wolff Proving Fairness and Implementation
Correctness of a Microkernel Scheduler 349--388
Eyad Alkassar and
Mark A. Hillebrand and
Dirk C. Leinenbach and
Norbert W. Schirmer and
Artem Starostin and
Alexandra Tsyban Balancing the Load . . . . . . . . . . . 389--454
Jasmin Christian Blanchette Proof Pearl: Mechanizing the Textbook
Proof of Huffman's Algorithm . . . . . . 1--18
Jean-François Dufourd An Intuitionistic Proof of a Discrete
Form of the Jordan Curve Theorem
Formalized in Coq with Combinatorial
Hypermaps . . . . . . . . . . . . . . . 19--51
Raúl Monroy and
Alan Bundy and
Ian Green On Process Equivalence = Equation
Solving in CCS . . . . . . . . . . . . . 53--80
Filip Mari\'c Formalization and Implementation of
Modern SAT Solvers . . . . . . . . . . . 81--119
K. Subramani Optimal Length Resolution Refutations of
Difference Constraint Systems . . . . . 121--137
Ruben A. Gamboa A Formalization of Powerlist Algebra in
ACL2 . . . . . . . . . . . . . . . . . . 139--172
Harald Zankl and
Nao Hirokawa and
Aart Middeldorp KBO Orientability . . . . . . . . . . . 173--201
G. Dalzotto and
T. Recio On Protocols for the Automated Discovery
of Theorems in Elementary Geometry . . . 203--236
Richard Boulton and
Joe Hurd and
Konrad Slind Computer Assisted Reasoning . . . . . . 237--242
John Harrison Formalizing an Analytic Proof of the
Prime Number Theorem . . . . . . . . . . 243--261
Sandrine Blazy and
Xavier Leroy Mechanized Semantics for the Clight
Subset of the C Language . . . . . . . . 263--288
Tobias Nipkow Social Choice Theory in HOL . . . . . . 289--304
Michael Norrish Rewriting Conversions Implemented with
Continuations . . . . . . . . . . . . . 305--336
Xavier Leroy A Formally Verified Compiler Back-end ??
Geoff Sutcliffe The TPTP Problem Library and Associated
Infrastructure . . . . . . . . . . . . . ??
Sascha Böhme and
Micha\l Moskal and
Wolfram Schulte and
Burkhart Wolff HOL-Boogie --- An Interactive
Prover-Backend for the Verifying C
Compiler . . . . . . . . . . . . . . . . ??
Jacques Carette and
Makarius Wenzel and
Freek Wiedijk Preface . . . . . . . . . . . . . . . . ??
Claudio Sacerdoti Coen Declarative Representation of Proof
Terms . . . . . . . . . . . . . . . . . ??
Dominik Dietrich and
Ewaryst Schulz Crystal: Integrating Structured Queries
into a Tactic Language . . . . . . . . . ??
Ferruccio Guidi Procedural Representation of CIC Proof
Terms . . . . . . . . . . . . . . . . . ??
Perry R. James and
Patrice Chalin Faster and More Complete Extended Static
Checking for the Java Modeling Language ??
Predrag Jani\vci\'c Geometry Constructions Language . . . . ??
Behzad Akbarpour and
Lawrence Charles Paulson MetiTarski: An Automatic Theorem Prover
for Real-Valued Special Functions . . . 175--205
Michael Mendler and
Stephan Scheele Towards Constructive DL for Abstraction
and Refinement . . . . . . . . . . . . . 207--243
Olivier Hermant Resolution is Cut-Free . . . . . . . . . 245--276
Knot Pipatsrisawat and
Adnan Darwiche On Modern Clause-Learning Satisfiability
Solvers . . . . . . . . . . . . . . . . 277--301
Alexander Krauss Partial and Nested Recursive Function
Definitions in Higher-order Logic . . . 303--336
Bernardo Cuenca Grau and
Christian Halaschek-Wiener and
Yevgeny Kazakov and
Boontawee Suntisrivaraporn Incremental Classification of
Description Logics Ontologies . . . . . 337--369
Mauro Ferrari and
Camillo Fiorentini and
Guido Fiorino $ \boldsymbol {\cal BC \! D \! L} $:
Basic Constructive Description Logic . . 371--399
Ruzica Piskac and
Leonardo de Moura and
Nikolaj Bjòrner Deciding Effectively Propositional Logic
Using DPLL and Substitution Sets . . . . 401--424
Yang Xiang and
Kevin Grant Preface: Special Issue on Uncertain
Reasoning . . . . . . . . . . . . . . . 1--2
Gabriele Kern-Isberner and
Manuela Ritterskamp Preference Fusion for Default Reasoning
Beyond System Z . . . . . . . . . . . . 3--19
Miguel A. Palacios-Alonso and
Carlos A. Brizuela and
L. Enrique Sucar Evolutionary Learning of Dynamic Naive
Bayesian Classifiers . . . . . . . . . . 21--37
Salem Benferhat and
Safa Yahi and
Habiba Drias A New Default Theories Compilation for
MSP--Entailment . . . . . . . . . . . . 39--59
Frédéric Pichon and
Thierry Den\oeux The Unnormalized Dempster's Rule of
Combination: A New Justification from
the Least Commitment Principle and Some
Extensions . . . . . . . . . . . . . . . 61--87
Alessandro Armando and
Peter Baumgartner and
Gilles Dowek Preface . . . . . . . . . . . . . . . . 89--89
Franz Baader and
Rafael Peñaloza Automata-Based Axiom Pinpointing . . . . 91--129
Marius Bozga and
Radu Iosif and
Swann Perarnau Quantitative Separation Logic and
Programs with Lists . . . . . . . . . . 131--156
Vivek Nigam and
Dale Miller A Framework for Proof Systems . . . . . 157--188
Tobias Nipkow Linear Quantifier Elimination . . . . . 189--212
Zheng Ye and
Shang-Ching Chou and
Xiao-Shan Gao Visually Dynamic Presentation of Proofs
in Plane Geometry . . . . . . . . . . . 213--241
Zheng Ye and
Shang-Ching Chou and
Xiao-Shan Gao Visually Dynamic Presentation of Proofs
in Plane Geometry . . . . . . . . . . . 243--266
James Cheney Equivariant Unification . . . . . . . . 267--300
André L. Galdino and
Mauricio Ayala-Rincón A Formalization of the
Knuth--Bendix(--Huet) Critical Pair
Theorem . . . . . . . . . . . . . . . . 301--325
Bernhard Beckert and
Reiner Hähnle Tests and Proofs . . . . . . . . . . . . 327--329
Andrea Calvagna and
Angelo Gargantini A Formal Logic Approach to Constrained
Combinatorial Testing . . . . . . . . . 331--358
Andriy Dunets and
Gerhard Schellhorn and
Wolfgang Reif Automated Flaw Detection in Algebraic
Specifications . . . . . . . . . . . . . 359--395
Damiano Angeletti and
Enrico Giunchiglia and
Massimo Narizzano and
Alessandra Puddu and
Salvatore Sabina Using Bounded Model Checking for
Coverage Analysis of Safety-Critical
Software in an Industrial Setting . . . 397--414
Lydie du Bousquet and
Yves Ledru and
Olivier Maury and
Catherine Oriat and
Jean-Louis Lanet Reusing a JML Specification Dedicated to
Verification for Testing, and
Vice-Versa: Case Studies . . . . . . . . 415--435
Delphine Longuet and
Marc Aiguier and
Pascale Le Gall Proof-Guided Test Selection from
First-Order Specifications with Equality 437--473
Carlos Areces and
Daniel Gorín Resolution with Order and Selection for
Hybrid Logics . . . . . . . . . . . . . 1--42
Szymon Klarman and
Ulle Endriss and
Stefan Schlobach ABox Abduction in the Description Logic
$ \boldsymbol \mathcal {ALC} $ . . . . . 43--80
Javier Larrosa and
Robert Nieuwenhuis and
Albert Oliveras and
Enric Rodríguez-Carbonell A Framework for Certified Boolean
Branch-and-Bound Optimization . . . . . 81--102
Ole J. Mengshoel and
Dan Roth and
David C. Wilkins Portfolios in Stochastic Local Search:
Efficiently Computing Most Probable
Explanations in Bayesian Networks . . . 103--160
Elvira Albert and
Puri Arenas and
Samir Genaim and
Germán Puebla Closed-Form Upper Bounds in Static Cost
Analysis . . . . . . . . . . . . . . . . 161--203
Antonio Hernando and
Eugenio Roanes-Lozano and
Luis M. Laita A Polynomial Model for Logics with a
Prime Power Number of Truth Values . . . 205--221
Lujo Bauer and
Sandro Etalle and
Jerry den Hartog and
Luca Vigan\`o Preface of Special Issue on ``Computer
Security: Foundations and Automated
Reasoning'' . . . . . . . . . . . . . . 223--224
Véronique Cortier and
Steve Kremer and
Bogdan Warinschi A Survey of Symbolic Methods in
Computational Analysis of Cryptographic
Systems . . . . . . . . . . . . . . . . 225--259
J. Courant and
M. Daubignard and
C. Ene and
P. Lafourcade and
Y. Lakhnech Automated Proofs for Asymmetric
Encryption . . . . . . . . . . . . . . . 261--291
Joana Martinho and
António Ravara Encoding Cryptographic Primitives in a
Calculus with Polyadic Synchronisation 293--323
Ralf Küsters and
Tomasz Truderung Reducing Protocol Analysis with XOR to
the XOR--Free Case in the Horn Theory
Based Approach . . . . . . . . . . . . . 325--352
Wihem Arsac and
Giampaolo Bella and
Xavier Chantry and
Luca Compagna Multi-Attacker Protocol Validation . . . 353--388
Max Kanovich and
Paul Rowe and
Andre Scedrov Collaborative Planning with
Confidentiality . . . . . . . . . . . . 389--421
Michael J. C. Gordon and
Matt Kaufmann and
Sandip Ray The Right Tools for the Job: Correctness
of Cone of Influence Reduction Proved
Using ACL2 and HOL4 . . . . . . . . . . 1--16
John Thangarajah and
Lin Padgham Computationally Effective Reasoning
About Goal Interactions . . . . . . . . 17--56
Louise Abigail Dennis and
Ian Green and
Alan Smaill The Use of Embeddings to Provide a Clean
Separation of Term and Annotation for
Higher Order Rippling . . . . . . . . . 57--105
Renate A. Schmidt and
Brigitte Pientka Preface: Special Issue of Selected
Extended Papers of CADE-22 . . . . . . . 107--109
Koen Claessen and
Ann Lillieström Automated Inference of Finite
Unsatisfiability . . . . . . . . . . . . 111--132
Carsten Fuhs and
Jürgen Giesl and
Michael Parting and
Peter Schneider-Kamp and
Stephan Swiderski Proving Termination by Dependency Pairs
and Inductive Theorem Proving . . . . . 133--160
Maria Paola Bonacina and
Christopher A. Lynch and
Leonardo de Moura On Deciding Satisfiability by Theorem
Proving with Speculative Inferences . . 161--189
Peter Baumgartner and
Uwe Waldmann A Combined Superposition and Model
Evolution Calculus . . . . . . . . . . . 191--227
Francisco Jesús Martín-Mateos and
José Luis Ruiz-Reina and
José Antonio Alonso and
María José Hidalgo Proof Pearl: a Formal Proof of Higman's
Lemma in ACL2 . . . . . . . . . . . . . 229--250
Moa Johansson and
Lucas Dixon and
Alan Bundy Conjecture Synthesis for Inductive
Theories . . . . . . . . . . . . . . . . 251--289
Amine Chaieb Formal Power Series . . . . . . . . . . 291--318
Gianni Ciolli and
Graziano Gentili and
Marco Maggesi A Certified Proof of the Cartan Fixed
Point Theorems . . . . . . . . . . . . . 319--336
Jürgen Giesl and
Reiner Hähnle Preface: Special Issue of Selected
Extended Papers of IJCAR 2010 . . . . . 337--339
Angelo Brillout and
Daniel Kroening and
Philipp Rümmer and
Thomas Wahl An Interpolating Sequent Calculus for
Quantifier-Free Presburger Arithmetic 341--367
Jasmin Christian Blanchette and
Alexander Krauss Monotonicity Inference for Higher-Order
Formulas . . . . . . . . . . . . . . . . 369--398
Hans de Nivelle Classical Logic with Partial Functions 399--425
Despoina Magka and
Yevgeny Kazakov and
Ian Horrocks Tractable Extensions of the Description
Logic $ {\mathcal {EL}} $ with Numerical
Datatypes . . . . . . . . . . . . . . . 427--450
Julian Backes and
Chad Edward Brown Analytic Tableaux for Higher-Order Logic
with Choice . . . . . . . . . . . . . . 451--479
Nao Hirokawa and
Aart Middeldorp Decreasing Diagrams and Relative
Termination . . . . . . . . . . . . . . 481--501
Daniele Zucchelli and
Enrica Nicolini A Decidability Result for the Model
Checking of Infinite-State Systems . . . 1--42
Amy Felty and
Alberto Momigliano Hybrid . . . . . . . . . . . . . . . . . 43--105
Cristina Borralleras and
Salvador Lucas and
Albert Oliveras and
Enric Rodríguez-Carbonell and
Albert Rubio SAT Modulo Linear Arithmetic for Solving
Polynomial Constraints . . . . . . . . . 107--131
Hubert Comon-Lundh and
Catherine Meadows Special Issue on Security and Rewriting
Foreword . . . . . . . . . . . . . . . . 133--134
Siva Anantharaman and
Hai Lin and
Christopher Lynch and
Paliath Narendran and
Michael Rusinowitch Unification Modulo Homomorphic
Encryption . . . . . . . . . . . . . . . 135--158
Joshua D. Guttman State and Progress in Strand Spaces:
Proving Fair Exchange . . . . . . . . . 159--195
Steve Kremer and
Antoine Mercier and
Ralf Treinen Reducing Equational Theories for the
Decision of Static Equivalence . . . . . 197--217
\cStefan Ciobâc\ua and
Stéphanie Delaune and
Steve Kremer Computing Knowledge in Security
Protocols Under Convergent Equational
Theories . . . . . . . . . . . . . . . . 219--262
Yannick Chevalier and
Michaël Rusinowitch Decidability of Equivalence of Symbolic
Derivations . . . . . . . . . . . . . . 263--292
Mnacho Echenim and
Nicolas Peltier An Instantiation Scheme for
Satisfiability Modulo Theories . . . . . 293--362
Jan Otop E-unification with Constants vs. General
E-unification . . . . . . . . . . . . . 363--390
Bela\"\id Benhamou and
Lionel Paris and
Pierre Siegel Dealing with Satisfiability and $n$-ary
CSPs in a Logical Framework . . . . . . 391--417
Freek Verbeek and
Julien Schmaltz Proof Pearl: A Formal Proof of Dally and
Seitz' Necessary and Sufficient
Condition for Deadlock-Free Routing in
Interconnection Networks . . . . . . . . 419--439
Véronique Cortier and
Stéphanie Delaune Decidability and Combination Results for
Two Notions of Knowledge in Security
Protocols . . . . . . . . . . . . . . . 441--487
Predrag Jani\vci\'c and
Julien Narboux and
Pedro Quaresma The Area Method . . . . . . . . . . . . 489--532
Liang Chang and
Zhongzhi Shi and
Tianlong Gu and
Lingzhong Zhao A Family of Dynamic Description Logics
for Representing and Reasoning About
Actions . . . . . . . . . . . . . . . . 1--52
Michael Codish and
Jürgen Giesl and
Peter Schneider-Kamp and
René Thiemann SAT Solving for Termination Proofs with
Recursive Path Orders and Dependency
Pairs . . . . . . . . . . . . . . . . . 53--93
Alexander Krauss and
Tobias Nipkow Proof Pearl: Regular Expression
Equivalence and Relation Algebra . . . . 95--106
Freek Wiedijk Book Review: \booktitleHandbook of
Practical Logic and Automated Reasoning,
by John R. Harrison, Cambridge
University Press, 2009 . . . . . . . . . 107--109
Maribel Fernández and
Christian Urban Preface: Theory and Applications of
Abstraction, Substitution and Naming . . 111--114
Matthew R. Lakin and
Andrew M. Pitts Encoding Abstract Syntax Without Fresh
Names . . . . . . . . . . . . . . . . . 115--140
Nick Benton and
Chung-Kil Hur and
Andrew J. Kennedy and
Conor McBride Strongly Typed Term Representations in
Coq . . . . . . . . . . . . . . . . . . 141--159
Filippo Bonchi and
Maria Grazia Buscemi and
Vincenzo Ciancia and
Fabio Gadducci A Presheaf Environment for the Explicit
Fusion Calculus . . . . . . . . . . . . 161--183
Randy Pollack and
Masahiko Sato and
Wilmer Ricciotti A Canonical Locally Named Representation
of Binding . . . . . . . . . . . . . . . 185--207
James Cheney and
Michael Norrish and
René Vestergaard Formalizing Adequacy: A Case Study for
Higher-order Abstract Syntax . . . . . . 209--239
Andrew Gacek and
Dale Miller and
Gopalan Nadathur A Two-Level Logic Approach to Reasoning
About Computations . . . . . . . . . . . 241--273
Kristoffer H. Rose and
Roel Bloo and
Frédéric Lang On Explicit Substitution with Names . . 275--300
Benjamin C. Pierce and
Stephanie Weirich Preface . . . . . . . . . . . . . . . . 301--302
Stefan Berghofer A Solution to the \sc PoplMark Challenge
Using de Bruijn Indices in Isabelle/HOL 303--326
Jérôme Vouillon A Solution to the \sc PoplMark Challenge
Based on de Bruijn Indices . . . . . . . 327--362
Arthur Charguéraud The Locally Nameless Representation . . 363--408
André Hirschowitz and
Marco Maggesi Nested Abstract Syntax in Coq . . . . . 409--426
Andrea Asperti and
Wilmer Ricciotti and
Claudio Sacerdoti Coen and
Enrico Tassi Formal Metatheory of Programming
Languages in the Matita Interactive
Theorem Prover . . . . . . . . . . . . . 427--451
Andrew W. Appel and
Robert Dockins and
Xavier Leroy A List-Machine Benchmark for Mechanized
Metatheory . . . . . . . . . . . . . . . 453--491
Steven Schockaert and
Jeroen Janssen and
Dirk Vermeir Satisfiability Checking in \Lukasiewicz
Logic as Finite Constraint Satisfaction 493--550
Jia Tao and
Giora Slutzki and
Vasant Honavar PS PACE Tableau Algorithms for Acyclic
Modalized $ \boldsymbol \mathcal {ALC} $ 551--582
Matti Järvisalo and
Armin Biere and
Marijn J. H. Heule Simulating Circuit-Level Simplifications
on CNF . . . . . . . . . . . . . . . . . 583--619
Jose Gaintzarain and
Montserrat Hermo and
Paqui Lucio and
Marisa Navarro and
Fernando Orejas Invariant-Free Clausal Temporal
Resolution . . . . . . . . . . . . . . . 1--49
Miquel Bofill and
Albert Rubio Paramodulation with Non-Monotonic
Orderings and Simplification . . . . . . 51--98
James P. Bridge and
Lawrence Charles Paulson Case Splitting in an Automatic Theorem
Prover for Real-Valued Special Functions 99--117
Andrzej Trybulec and
Artur Kornilowicz and
Adam Naumowicz and
Krystyna Kuperberg Formal Mathematics for Mathematicians 119--121
Jesse Alama Eliciting Implicit Assumptions of Mizar
Proofs by Property Omission . . . . . . 123--133
Johan G. F. Belinfante The GOEDEL Program . . . . . . . . . . . 135--146
Marco Bright Caminati and
Giuseppe Rosolini Custom Automations in Mizar . . . . . . 147--160
Yuichi Futa and
Hiroyuki Okazaki and
Yasunari Shidama Formalization of Definitions and
Theorems Related to an Elliptic Curve
Over a Finite Prime Field by Using Mizar 161--172
John Harrison The HOL Light Theory of Euclidean Space 173--190
Mihnea Iancu and
Michael Kohlhase and
Florian Rabe and
Josef Urban The Mizar Mathematical Library in OMDoc:
Translation and Applications . . . . . . 191--202
Artur Korni\l owicz On Rewriting Rules in Mizar . . . . . . 203--210
Jan Mycielski On the Formalization of Theories . . . . 211--216
Karol P\kak Methods of Lemma Extraction in Natural
Deduction Proofs . . . . . . . . . . . . 217--228
Josef Urban and
Piotr Rudnicki and
Geoff Sutcliffe ATP and Presentation Service for Mizar
Formalizations . . . . . . . . . . . . . 229--241
Clark Barrett and
Morgan Deters and
Leonardo de Moura and
Albert Oliveras and
Aaron Stump 6 Years of SMT--COMP . . . . . . . . . . 243--277
Nao Hirokawa and
Aart Middeldorp and
Harald Zankl Uncurrying for Termination and
Complexity . . . . . . . . . . . . . . . 279--315
Sarah Winkler and
Haruhiko Sato and
Aart Middeldorp and
Masahito Kurihara Multi-Completion with Termination Tools 317--354
Rajeev Goré and
Linh Anh Nguyen ExpTime Tableaux for Using Sound Global
Caching . . . . . . . . . . . . . . . . 355--381
David Sabel and
Manfred Schmidt-Schauß A Two-Valued Logic for Properties of
Strict Functional Programs Allowing
Partial Functions . . . . . . . . . . . 383--421
Sylvie Boldo and
François Clément and
Jean-Christophe Filliâtre and
Micaela Mayero and
Guillaume Melquiond and
Pierre Weis Wave Equation Numerical Resolution: a
Comprehensive Mechanized Proof of a C
Program . . . . . . . . . . . . . . . . 423--456
Nikolaj Bjòrner and
Viorica Sofronie-Stokkermans Preface: Special Issue of Selected
Extended Papers of CADE-23 . . . . . . . 1--2
Didier Galmiche and
Daniel Méry A Connection-based Characterization of
Bi-intuitionistic Validity . . . . . . . 3--26
Lars Noschinski and
Fabian Emmes and
Jürgen Giesl Analyzing Innermost Runtime Complexity
of Term Rewriting by Dependency Pairs 27--56
Chad E. Brown Reducing Higher-Order Theorem Proving to
a Sequence of SAT Problems . . . . . . . 57--77
Dejan Jovanovi\'c and
Leonardo de Moura Cutting to the Chase . . . . . . . . . . 79--108
Jasmin Christian Blanchette and
Sascha Böhme and
Lawrence C. Paulson Extending Sledgehammer with SMT Solvers 109--128
Mauro Ferrari and
Camillo Fiorentini and
Guido Fiorino Contraction-Free Linear Depth Sequent
Calculi for Intuitionistic Propositional
Logic with the Subformula Property and
Minimal Depth Counter-Models . . . . . . 129--149
César Muñoz and
Anthony Narkawicz Formalization of Bernstein Polynomials
and Applications to Global Optimization 151--196
Serenella Cerrito and
Marta Cialdea Mayer A Tableau Based Decision Procedure for
an Expressive Fragment of Hybrid Logic
with Binders, Converse and Global
Modalities . . . . . . . . . . . . . . . 197--239
Sandip Ray and
Rob Sumners Specification and Verification of
Concurrent Programs Through Refinements 241--280
Carles Creus and
Guillem Godoy and
Francesc Massanes and
Ashish Tiwari Non-Linear Rewrite Closure and Weak
Normalization . . . . . . . . . . . . . 281--324
Christopher Lynch and
Quang-Trung Ta and
Duc-Khanh Tran SMELS: Satisfiability Modulo Equality
with Lazy Superposition . . . . . . . . 325--356
Christian Sternagel Proof Pearl--- A Mechanized Proof of
GHC's Mergesort . . . . . . . . . . . . 357--370
Carles Creus and
Adri\`a Gascón and
Guillem Godoy Emptiness and Finiteness for Tree
Automata with Global Reflexive
Disequality Constraints . . . . . . . . 371--400
Matthias Baaz and
Ori Lahav and
Anna Zamansky Finite-valued Semantics for Canonical
Labelled Calculi . . . . . . . . . . . . 401--430
Alexei Lisitsa Finite Reasons for Safety . . . . . . . 431--451
Clark Barrett Book Review: \booktitleDecision
Procedures: An Algorithmic Point of
View, by Daniel Kroening and Ofer
Strichman, Springer--Verlag, 2008 . . . 453--456
Eugenio G. Omodeo and
Alexandru I. Tomescu Set Graphs. III. Proof Pearl: Claw-Free
Graphs Mirrored into Transitive
Hereditarily Finite Sets . . . . . . . . 1--29
Matthew Gwynne and
Oliver Kullmann Generalising Unit-Refutation
Completeness and SLUR via Nested Input
Resolution . . . . . . . . . . . . . . . 31--65
Guido Fiorino Terminating Calculi for Propositional
Dummett Logic with Subformula Property 67--97
Marta R. Hidalgo and
Robert Joan-Arinyo The Reachability Problem in Constructive
Geometric Constraint Solving Based
Dynamic Geometry . . . . . . . . . . . . 99--122
Clemens Ballarin Locales: A Module System for
Mathematical Theories . . . . . . . . . 123--153
Temur Kutsia and
Jordi Levy and
Mateu Villaret Anti-unification for Unranked Terms and
Hedges . . . . . . . . . . . . . . . . . 155--190
Jesse Alama and
Tom Heskes and
Daniel Kühlwein and
Evgeni Tsivtsivadze and
Josef Urban Premise Selection for Mathematics by
Corpus Analysis and Kernel Methods . . . 191--213
Jonghyun Park and
Jeongbong Seo and
Sungwoo Park and
Gyesik Lee Mechanizing Metatheory Without Typing
Contexts . . . . . . . . . . . . . . . . 215--239
Eyad Alkassar and
Sascha Böhme and
Kurt Mehlhorn and
Christine Rizkallah A Framework for the Verification of
Certifying Computations . . . . . . . . 241--273
Alexander Malkis and
Anindya Banerjee On Automation in the Verification of
Software Barriers: Experience Report . . 275--329
M. J. Hidalgo-Doblado and
J. A. Alonso-Jiménez and
J. Borrego-Díaz and
F. J. Martín-Mateos and
J. L. Ruiz-Reina Formally Verified Tableau-Based
Reasoners for a Description Logic . . . 331--360
Mike Stannett and
István Németi Using Isabelle/HOL to Verify First-Order
Relativity Theory . . . . . . . . . . . 361--378
Min Zhou and
Fei He and
Bow-Yaw Wang and
Ming Gu and
Jiaguang Sun Array Theory of Bounded Elements and its
Applications . . . . . . . . . . . . . . 379--405
Mark Kaminski and
Gert Smolka A Goal-Directed Decision Procedure for
Hybrid PDL . . . . . . . . . . . . . . . 407--450
Chunhan Wu and
Xingyuan Zhang and
Christian Urban A Formalisation of the Myhill--Nerode
Theorem Based on Regular Expressions . . 451--480
Yevgeny Kazakov and
Markus Krötzsch and
Franti\vsek Siman\vcík The Incredible ELK . . . . . . . . . . . 1--61
Reynald Affeldt and
Manabu Hagiwara and
Jonas Sénizergues Formalization of Shannon's Theorems . . 63--103
Julianna Zsidó Theorem of Three Circles in Coq . . . . 105--127
Stijn de Gouw and
Frank de Boer and
Jurriaan Rot Proof Pearl: The KeY to Correct and
Stable Sorting . . . . . . . . . . . . . 129--139
James P. Bridge and
Sean B. Holden and
Lawrence C. Paulson Machine Learning for First-Order Theorem
Proving . . . . . . . . . . . . . . . . 141--172
Cezary Kaliszyk and
Josef Urban Learning-Assisted Automated Reasoning
with Flyspeck . . . . . . . . . . . . . 173--213
Jiewen Wu and
Alexander Hudek and
David Toman and
Grant Weddell Absorption for ABoxes . . . . . . . . . 215--243
Birte Glimm and
Ian Horrocks and
Boris Motik and
Giorgos Stoilos and
Zhe Wang HermiT: An OWL 2 Reasoner . . . . . . . 245--269
Thomas Braibant and
Jacques-Henri Jourdan and
David Monniaux Implementing and Reasoning About
Hash-consed Data Structures in Coq . . . 271--304
Marta Cialdea Mayer Extended Decision Procedure for a
Fragment of HL with Binders . . . . . . 305--315
Hicham Bensaid and
Nicolas Peltier A Complete Superposition Calculus for
Primal Grammars . . . . . . . . . . . . 317--350
Andreas Steigmiller and
Birte Glimm and
Thorsten Liebig Reasoning with Nominal Schemas through
Absorption . . . . . . . . . . . . . . . 351--405
Umair Siddique and
Osman Hasan On the Formalization of Gamma Function
in HOL . . . . . . . . . . . . . . . . . 407--429
Érik Martin-Dorel and
Guillaume Hanrot and
Micaela Mayero and
Laurent Théry Formally Verified Certificate Checkers
for Hardest-to-Round Computation . . . . 1--29
Kamalesh Ghosh and
Pallab Dasgupta and
S. Ramesh Automated Planning as an Early
Verification Tool for Distributed
Control . . . . . . . . . . . . . . . . 31--68
Maria Paola Bonacina and
Moa Johansson On Interpolation in Automated Theorem
Proving . . . . . . . . . . . . . . . . 69--97
Cezary Kaliszyk and
Josef Urban Erratum to: Learning-Assisted Automated
Reasoning with Flyspeck . . . . . . . . 99--99
Harald Zankl and
Bertram Felgenhauer and
Aart Middeldorp Labelings for Decreasing Diagrams . . . 101--133
Sylvie Boldo and
Jacques-Henri Jourdan and
Xavier Leroy and
Guillaume Melquiond Verified Compilation of Floating-Point
Computations . . . . . . . . . . . . . . 135--163
Simon Foster and
Georg Struth On the Fine-Structure of Regular Algebra 165--197
Bernhard Reus and
Nathaniel Charlton and
Ben Horsfall Symbolic Execution Proofs for Higher
Order Store Programs . . . . . . . . . . 199--284
Anthony Narkawicz and
César Muñoz and
Aaron Dutle Formally-Verified Decision Procedures
for Univariate Polynomial Computation
Based on Sturm's and Tarski's Theorems 285--326
Francesco Alberti and
Silvio Ghilardi and
Natasha Sharygina Decision Procedures for Flat Array
Properties . . . . . . . . . . . . . . . 327--352
Maria Paola Bonacina and
Moa Johansson Interpolation Systems for Ground Proofs
in Automated Deduction: a Survey . . . . 353--390
Lawrence C. Paulson A Mechanised Proof of Gödel's
Incompleteness Theorems Using Nominal
Isabelle . . . . . . . . . . . . . . . . 1--37
Francisco Botana and
Markus Hohenwarter and
Predrag Jani\vci\'c and
Zoltán Kovács and
Ivan Petrovi\'c and
Tomás Recio and
Simon Weitzhofer Automated Theorem Proving in GeoGebra:
Current Achievements . . . . . . . . . . 39--59
David R. Cok and
Aaron Stump and
Tjark Weber The 2013 Evaluation of SMT--COMP and
SMT--LIB . . . . . . . . . . . . . . . . 61--90
Daniel Kühlwein and
Josef Urban MaLeS: A Framework for Automatic Tuning
of Automated Theorem Provers . . . . . . 91--116
Jared Davis and
Magnus O. Myreen The Reflective Milawa Theorem Prover is
Sound (Down to the Machine Code that
Runs it) . . . . . . . . . . . . . . . . 117--183
Marta Cialdea Mayer Erratum to: ``Extension of a Decision
Procedure for a Fragment of Hybrid Logic
with Binders'' . . . . . . . . . . . . . 185--185
Krystyna Trybulec Kuperberg Andrzej Trybulec --- in Memoriam . . . . 187--190
Adam Grabowski and
Artur Korni\l owicz and
Adam Naumowicz Four Decades of Mizar . . . . . . . . . 191--198
Chad E. Brown Reconsidering Pairs and Functions as
Sets . . . . . . . . . . . . . . . . . . 199--210
Adam Grabowski Mechanizing Complemented Lattices Within
Mizar Type System . . . . . . . . . . . 211--221
John Harrison Formal Proofs of Hypergeometric Sums . . 223--243
Cezary Kaliszyk and
Josef Urban MizAR 40 for Mizar 40 . . . . . . . . . 245--256
Artur Korni\l owicz Definitional Expansions in Mizar . . . . 257--268
Alexander Lyaletski Evidence Algorithm and Inference Search
in First-Order Logics . . . . . . . . . 269--284
Adam Naumowicz Automating Boolean Set Operations in
Mizar Proof Checking with the Aid of an
External SAT Solver . . . . . . . . . . 285--294
Karol P\kak Improving Legibility of Formal Proofs
Based on the Close Reference Principle
is NP--Hard . . . . . . . . . . . . . . 295--306
Amy P. Felty and
Alberto Momigliano and
Brigitte Pientka The Next 700 Challenge Problems for
Reasoning with Higher-Order Abstract
Syntax Representations . . . . . . . . . 307--372
Andrea Asperti Reverse Complexity . . . . . . . . . . . 373--388
Christoph Benzmüller and
Nik Sultana and
Lawrence C. Paulson and
Frank Theiß The Higher-Order Prover Leo-II . . . . . 389--404
Jesper Bengtson and
Joachim Parrow and
Tjark Weber Psi-Calculi in Isabelle . . . . . . . . 1--47
Martin Gagné and
Pascal Lafourcade and
Yassine Lakhnech and
Reihaneh Safavi-Naini Automated Proofs of Block Cipher Modes
of Operation . . . . . . . . . . . . . . 49--94
Peter Baumgartner and
Wolfgang Bibel and
Richard Waldinger In Memory of Mark Stickel . . . . . . . 95--98
Donald W. Loveland Mark Stickel: His Earliest Work . . . . 99--112
Maria Paola Bonacina and
David A. Plaisted Semantically-Guided Goal-Sensitive
Reasoning: Model Representation . . . . 113--141
Hantao Zhang An Experiment with Satisfiability Modulo
SAT . . . . . . . . . . . . . . . . . . 143--154
Jasmin Christian Blanchette and
Sascha Böhme and
Mathias Fleury and
Steffen Juilf Smolka and
Albert Steckermeier Semi-intelligible Isar Proofs from
Machine-Generated Proofs . . . . . . . . 155--200
Gerwin Klein and
Ruben Gamboa Interactive Theorem Proving . . . . . . 201--203
Rob Arthan On Definitions of Constants and Types in
HOL . . . . . . . . . . . . . . . . . . 205--219
Ramana Kumar and
Rob Arthan and
Magnus O. Myreen and
Scott Owens Self-Formalisation of Higher-Order Logic 221--259
Daniel Matichuk and
Toby Murray and
Makarius Wenzel Eisbach: A Proof Method Language for
Isabelle . . . . . . . . . . . . . . . . 261--282
Sandrine Blazy and
Vincent Laporte and
David Pichardie Verified Abstract Interpretation
Techniques for Disassembling Low-level
Self-modifying Code . . . . . . . . . . 283--308
Timothy Bourke and
Robert J. van Glabbeek and
Peter Höfner Mechanizing a Process Algebra for
Network Protocols . . . . . . . . . . . 309--341
Christian Doczkal and
Gert Smolka Completeness and Decidability Results
for CTL in Constructive Type Theory . . 343--365
Jeremy Avigad and
Robert Y. Lewis and
Cody Roux A Heuristic Prover for Real Inequalities 367--386
Claire Dross and
Sylvain Conchon and
Johannes Kanig and
Andrei Paskevich Adding Decision Procedures to SMT
Solvers Using Axioms with Triggers . . . 387--457
Friedrich Slivovsky and
Stefan Szeider Quantifier Reordering for QBF . . . . . 459--477
Daniel Kroening and
Andrey Rybalchenko Preface: Special Issue on Interpolation 1--2
Matthias Schlaipfer and
Georg Weissenbacher Labelled Interpolation Systems for
Hyper-Resolution, Clausal, and Local
Proofs . . . . . . . . . . . . . . . . . 3--36
Nishant Totla and
Thomas Wies Complete Instantiation-Based
Interpolation . . . . . . . . . . . . . 37--65
Jürgen Christ and
Jochen Hoenicke Proof Tree Preserving Tree Interpolation 67--95
M. Echenim and
N. Peltier A Superposition Calculus for Abductive
Reasoning . . . . . . . . . . . . . . . 97--134
Pierre Roux Formal Proofs of Rounding Error Bounds:
With Application to an Automatic
Positive Definiteness Check . . . . . . 135--156
Peter Franek and
Stefan Ratschan and
Piotr Zgliczynski Quasi-decidability of a Fragment of the
First-Order Theory of Real Numbers . . . 157--185
Érik Martin-Dorel and
Guillaume Melquiond Proving Tight Bounds on Univariate
Expressions with Elementary Functions in
Coq . . . . . . . . . . . . . . . . . . 187--217
Jasmin Christian Blanchette and
David Greenaway and
Cezary Kaliszyk and
Daniel Kühlwein and
Josef Urban A Learning-Based Fact Selector for
Isabelle/HOL . . . . . . . . . . . . . . 219--244
Thierry Boy de la Tour and
Nicolas Peltier Proof Generalization in LK by Second
Order Unifier Minimization . . . . . . . 245--280
Tuan-Hung Pham and
Andrew Gacek and
Michael W. Whalen Reasoning About Algebraic Data Types
with Abstractions . . . . . . . . . . . 281--318
Robbert Krebbers A Formal C Memory Model for Separation
Logic . . . . . . . . . . . . . . . . . 319--387
Stéphane Demri and
Deepak Kapur and
Christoph Weidenbach Preface . . . . . . . . . . . . . . . . 1--2
Jürgen Giesl and
Cornelius Aschermann and
Marc Brockschmidt and
Fabian Emmes and
Florian Frohn and
Carsten Fuhs and
Jera Hensel and
Carsten Otto and
Martin Plücker and
Peter Schneider-Kamp and
Thomas Ströder and
Stephanie Swiderski and
René Thiemann Analyzing Program Termination and
Complexity Automatically with AProVE . . 3--31
Thomas Ströder and
Jürgen Giesl and
Marc Brockschmidt and
Florian Frohn and
Carsten Fuhs and
Jera Hensel and
Peter Schneider-Kamp and
Cornelius Aschermann Automatically Proving Termination and
Memory Safety for Programs with Pointer
Arithmetic . . . . . . . . . . . . . . . 33--65
\.Ismail \.Ilkan Ceylan and
Rafael Peñaloza The Bayesian Ontology Language $
\mathcal {BEL} $ . . . . . . . . . . . . 67--95
Marijn J. H. Heule and
Martina Seidl and
Armin Biere Solution Validation and Extraction for
QBF Preprocessing . . . . . . . . . . . 97--125
Aleksandar Zelji\'c and
Christoph M. Wintersteiger and
Philipp Rümmer An Approximation Framework for Solvers
and Decision Procedures . . . . . . . . 127--147
Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel Soundness and Completeness Proofs by
Coinductive Methods . . . . . . . . . . 149--179
Michael Beeson and
Larry Wos Finding Proofs in Tarskian Geometry . . 181--207
Gabriel Braun and
Julien Narboux A Synthetic Proof of Pappus' Theorem in
Tarski's Geometry . . . . . . . . . . . 209--230
Ana Cristina Rocha-Oliveira and
André Luiz Galdino and
Mauricio Ayala-Rincón Confluence of Orthogonal Term Rewriting
Systems in the Prototype Verification
System . . . . . . . . . . . . . . . . . 231--251
M. Ganesalingam and
W. T. Gowers A Fully Automatic Theorem Prover with
Human-Style Output . . . . . . . . . . . 253--291
Alexander Baumgartner and
Temur Kutsia and
Jordi Levy and
Mateu Villaret Higher-Order Pattern Anti-Unification in
Linear Time . . . . . . . . . . . . . . 293--310
Amy Felty and
Aart Middeldorp Preface: Selected Extended Papers of
CADE 2015 . . . . . . . . . . . . . . . 311--312
Edward Zulkoski and
Curtis Bright and
Albert Heinle and
Ilias Kotsireas and
Krzysztof Czarnecki and
Vijay Ganesh Combining SAT Solvers with Computer
Algebra Systems to Verify Combinatorial
Conjectures . . . . . . . . . . . . . . 313--339
Andrew Reynolds and
Jasmin Christian Blanchette A Decision Procedure for (Co)datatypes
in SMT Solvers . . . . . . . . . . . . . 341--362
Vijay D'Silva and
Caterina Urban Abstract Interpretation as Automated
Deduction . . . . . . . . . . . . . . . 363--390
José Iborra and
Naoki Nishida and
Germán Vidal and
Akihisa Yamada Relative Termination via Dependency
Pairs . . . . . . . . . . . . . . . . . 391--411
Jean-Marie Lagniez and
Pierre Marquis On Preprocessing Techniques and Their
Impact on Propositional Model Counting 413--481
Manuel Eberl Proving Divide and Conquer Complexities
in Isabelle/HOL . . . . . . . . . . . . 483--508
Jesús Aransay and
Jose Divasón A Formalisation in HOL of the
Fundamental Theorem of Linear Algebra
and Its Application to the Solution of
the Least Squares Problem . . . . . . . 509--535
Jürgen Giesl and
Jan Hoffmann Preface: Special Issue on Automatic
Resource Bound Analysis . . . . . . . . 1--2
Moritz Sinn and
Florian Zuleger and
Helmut Veith Complexity and Resource Bound Analysis
of Imperative Programs Using Difference
Constraints . . . . . . . . . . . . . . 3--45
Elvira Albert and
Antonio Flores-Montoya and
Samir Genaim and
Enrique Martin-Martin Rely-Guarantee Termination and Cost
Analyses of Loops with Concurrent
Interleavings . . . . . . . . . . . . . 47--85
Steffen Jost and
Pedro Vasconcelos and
Mário Florido and
Kevin Hammond Type-Based Cost Analysis for Lazy
Functional Languages . . . . . . . . . . 87--120
Florian Frohn and
Jürgen Giesl and
Jera Hensel and
Cornelius Aschermann and
Thomas Ströder Lower Bounds for Runtime Complexity of
Term Rewriting . . . . . . . . . . . . . 121--163
Maria Paola Bonacina and
David A. Plaisted Semantically-Guided Goal-Sensitive
Reasoning: Inference System and
Completeness . . . . . . . . . . . . . . 165--218
André Platzer A Complete Uniform Substitution Calculus
for Differential Dynamic Logic . . . . . 219--265
Christoph Walther and
Nathan Wasser Fermat, Euler, Wilson --- Three Case
Studies in Number Theory . . . . . . . . 267--286
Zakaria Chihani and
Dale Miller and
Fabien Renaud A Semantic Framework for Proof Evidence 287--330
Jie Zhou and
Dingkang Wang and
Yao Sun Automated Reducible Geometric Theorem
Proving and Discovery by Gröbner Basis
Method . . . . . . . . . . . . . . . . . 331--344
Johannes Hölzl Markov Chains and Markov Decision
Processes in Isabelle/HOL . . . . . . . 345--387
Jeremy Avigad and
Johannes Hölzl and
Luke Serafin A Formally Verified Proof of the Central
Limit Theorem . . . . . . . . . . . . . 389--423
Luís Cruz-Filipe and
Kim S. Larsen and
Peter Schneider-Kamp Formally Proving Size Optimality of
Sorting Networks . . . . . . . . . . . . 425--454
Bijan Parsia and
Nicolas Matentzoglu and
Rafael S. Gonçalves and
Birte Glimm and
Andreas Steigmiller The OWL Reasoner Evaluation (ORE) 2015
Competition Report . . . . . . . . . . . 455--482
Geoff Sutcliffe The TPTP Problem Library and Associated
Infrastructure . . . . . . . . . . . . . 483--502
César A. Muñoz and
Sanjai Rayadurgam and
Oksana Tkachuk Selected Extended Papers of NFM 2016:
Preface . . . . . . . . . . . . . . . . 1--2
Julian Brunner and
Peter Lammich Formal Verification of an Executable LTL
Model Checker with Partial Order
Reduction . . . . . . . . . . . . . . . 3--21
Shaobo He and
Shuvendu K. Lahiri and
Zvonimir Rakamari\'c Verifying Relative Safety, Accuracy, and
Termination for Program Approximations 23--42
Susmit Jha and
Vasumathi Raman and
Dorsa Sadigh and
Sanjit A. Seshia Safe Autonomy Under Perception
Uncertainty Using Chance-Constrained
Temporal Logic . . . . . . . . . . . . . 43--62
Josh Newell and
Linna Pang and
David Tremaine and
Alan Wassyng and
Mark Lawford Translation of IEC 61131-3 Function
Block Diagrams to PVS for Formal
Verification with Real-Time Nuclear
Application . . . . . . . . . . . . . . 63--84
Muhammad Usama Sardar and
Nida Afaq and
Osman Hasan and
Khaza Anuarul Hoque Towards Probabilistic Formal Analysis of
SATS--Simultaneously Moving Aircraft
(SATS--SMA) . . . . . . . . . . . . . . 85--105
Yi-Chin Wu and
Vasumathi Raman and
Blake C. Rawlings and
Stéphane Lafortune and
Sanjit A. Seshia Synthesis of Obfuscation Policies to
Ensure Privacy and Utility . . . . . . . 107--131
John Slaney and
Bruno Woltzenlogel Paleo Conflict Resolution: A First-Order
Resolution Calculus with Decision
Literals and Conflict-Driven Clause
Learning . . . . . . . . . . . . . . . . 133--156
Zoltan A. Kocsis and
Jerry Swan Genetic Programming $ \varvec {+} $
Proof Search $ \varvec { = } $ Automatic
Improvement . . . . . . . . . . . . . . 157--176
Laura Bozzelli and
César Sánchez Visibly Linear Temporal Logic . . . . . 177--220
Filipe Casal and
João Rasga Many-Sorted Equivalence of Shiny and
Strongly Polite Theories . . . . . . . . 221--236
Marco Maggesi A Formalization of Metric Spaces in HOL
Light . . . . . . . . . . . . . . . . . 237--254
Sandrine Blazy and
Marsha Chechik Selected Extended Papers of VSTTE 2016 255--256
Gang Tan and
Greg Morrisett Bidirectional Grammars for Machine-Code
Decoding and Encoding . . . . . . . . . 257--277
Kensuke Kojima and
Akifumi Imanishi and
Atsushi Igarashi Automated Verification of Functional
Correctness of Race-Free GPU Programs 279--298
Dirk Beyer and
Matthias Dangl and
Philipp Wendler A Unifying View on SMT-Based Software
Verification . . . . . . . . . . . . . . 299--335
Moritz Kiefer and
Vladimir Klebanov and
Mattias Ulbrich Relational Program Reasoning Using
Compiler IR . . . . . . . . . . . . . . 337--363
Martin Clochard and
Léon Gondelman and
Mário Pereira The Matrix Reproved (Verification Pearl) 365--383
Nicolas Matentzoglu and
Bijan Parsia and
Uli Sattler OWL Reasoning: Subsumption Test Hardness
and Modularity . . . . . . . . . . . . . 385--419
Luis Aguirre and
Narciso Martí-Oliet and
Miguel Palomino and
Isabel Pita Sentence-Normalized Conditional
Narrowing Modulo in Rewriting Logic and
Maude . . . . . . . . . . . . . . . . . 421--463
Salvador Lucas and
Raúl Gutiérrez Automatic Synthesis of Logical Models
for Order-Sorted First-Order Theories 465--501
Eric Braude and
Satbek Abdyldayev Generalizing Morley's and Other Theorems
with Automated Realization . . . . . . . 503--526
John Slaney and
Bruno Woltzenlogel Paleo Erratum to: Conflict Resolution: A
First-Order Resolution Calculus with
Decision Literals and Conflict-Driven
Clause Learning . . . . . . . . . . . . 527--527
Jeremy Avigad and
Jasmin Christian Blanchette and
Gerwin Klein and
Lawrence Paulson and
Andrei Popescu and
Gregor Snelting Introduction to Milestones in
Interactive Theorem Proving . . . . . . 1--8
Grzegorz Bancerek and
Czes\law Byli\'nski and
Adam Grabowski and
Artur Korni\lowicz and
Roman Matuszewski and
Adam Naumowicz and
Karol P\kak The Role of the Mizar Mathematical
Library for Interactive Proof
Development in Mizar . . . . . . . . . . 9--32
Yves Bertot and
Laurence Rideau and
Laurent Théry Distant Decimals of $ \pi $: Formal
Proofs of Some Algorithms Computing Them
and Guarantees of Exact Computation . . 33--71
Fabian Immler A Verified ODE Solver and the Lorenz
Attractor . . . . . . . . . . . . . . . 73--111
Thomas Bauereiß and
Armando Pesenti Gritti and
Andrei Popescu and
Franco Raimondi CoSMed: A Confidentiality-Verified
Social Media Platform . . . . . . . . . 113--139
Hao Chen and
Xiongnan Wu and
Zhong Shao and
Joshua Lockerman and
Ronghui Gu Toward Compositional Verification of
Interruptible OS Kernels and Device
Drivers . . . . . . . . . . . . . . . . 141--189
Cornelius Diekmann and
Lars Hupel and
Julius Michaelis and
Maximilian Haslbeck and
Georg Carle Verified iptables Firewall Analysis and
Verification . . . . . . . . . . . . . . 191--242
Andreas Lochbihler Mechanising a Type-Safe Model of
Multithreaded Java with a Verified
Compiler . . . . . . . . . . . . . . . . 243--332
Jasmin Christian Blanchette and
Mathias Fleury and
Peter Lammich and
Christoph Weidenbach A Verified SAT Solver Framework with
Learn, Forget, Restart, and
Incrementality . . . . . . . . . . . . . 333--365
Qinxiang Cao and
Lennart Beringer and
Samuel Gruetter and
Josiah Dodds and
Andrew W. Appel VST-Floyd: A Separation Logic Tool to
Verify Correctness of C Programs . . . . 367--422
\Lukasz Czajka and
Cezary Kaliszyk Hammer for Coq: Automation for Dependent
Type Theory . . . . . . . . . . . . . . 423--453
Anders Schlichtkrull Formalization of the Resolution Calculus
for First-Order Logic . . . . . . . . . 455--484
Mohammad Abdulaziz and
Michael Norrish and
Charles Gretton Formally Verified Algorithms for
Upper-Bounding State Space Diameters . . 485--520
Christian Doczkal and
Gert Smolka Regular Language Representations in the
Constructive Type Theory of Coq . . . . 521--553
Pierre Boutry and
Charly Gries and
Julien Narboux and
Pascal Schreck Parallel Postulates and Continuity
Axioms: A Mechanized Study in
Intuitionistic Logic Using Coq . . . . . 1--68
Wenda Li and
Grant Olney Passmore and
Lawrence C. Paulson Deciding Univariate Polynomial Problems
Using Untrusted Certificates in
Isabelle\slash HOL . . . . . . . . . . . 69--91
Stijn de Gouw and
Frank S. de Boer and
Richard Bubel Verifying OpenJDK's Sort Method for
Generic Collections . . . . . . . . . . 93--126
Mauro Ferrari and
Camillo Fiorentini Goal-Oriented Proof-Search in Natural
Deduction for Intuitionistic
Propositional Logic . . . . . . . . . . 127--167
Jasmin Christian Blanchette and
Stephan Merz Selected Extended Papers of ITP 2016:
Preface . . . . . . . . . . . . . . . . 169--170
Hing-Lun Chan and
Michael Norrish Proof Pearl: Bounding Least Common
Multiples with Triangles . . . . . . . . 171--192
Thomas Grégoire and
Adam Chlipala Mostly Automated Formal Verification of
Loop Dependencies with Applications to
Distributed Stencil Algorithms . . . . . 193--213
Fabian Immler and
Christoph Traut The Flow of ODEs: Formalization of
Variational Equation and Poincaré Map . . 215--236
Ond\vrej Kun\vcar and
Andrei Popescu From Types to Sets by Local Type
Definition in Higher-Order Logic . . . . 237--260
Peter Lammich and
S. Reza Sefidgar Formalizing Network Flow Algorithms: a
Refinement Approach in Isabelle/HOL . . 261--280
Assia Mahboubi and
Guillaume Melquiond and
Thomas Sibut-Pinote Formally Verified Approximations of
Definite Integrals . . . . . . . . . . . 281--300
Filip Mari\'c Fast Formal Proof of the
Erd\Hos--Szekeres Conjecture for Convex
Polygons with at Most $6$ Points . . . . 301--329
Arthur Charguéraud and
François Pottier Verifying the Correctness and Amortized
Complexity of a Union--Find
Implementation in Separation Logic with
Time Credits . . . . . . . . . . . . . . 331--365
Tobias Nipkow and
Hauke Brinkop Amortized Complexity Verified . . . . . 367--391
Alexander Leitsch and
Anela Lolic Extraction of Expansion Trees . . . . . 393--430
Xingyuan Zhang and
Christian Urban Selected Extended Papers of ITP 2015:
Preface . . . . . . . . . . . . . . . . 431--432
Frédéric Besson and
Sandrine Blazy and
Pierre Wilke A Verified CompCert Front-End for a
Memory Model Supporting Pointer
Arithmetic and Uninitialised Data . . . 433--480
Peter Lammich Refinement to Imperative HOL . . . . . . 481--503
Sylvain Boulmé and
Alexandre Maréchal Refinement to Certify Abstract
Interpretations: Illustrated on
Linearization for Polyhedra . . . . . . 505--530
Ond\vrej Kun\vcar and
Andrei Popescu A Consistent Foundation for Isabelle/HOL 531--555
Gilles Barthe and
Gustavo Betarte and
Juan Diego Campo and
Carlos Luna System-Level Non-interference of
Constant-Time Cryptography. Part I:
Model . . . . . . . . . . . . . . . . . 1--51
Peter Lammich and
Andreas Lochbihler Automatic Refinement to Efficient Data
Structures: a Comparison of Two
Approaches . . . . . . . . . . . . . . . 53--94
Gabriel Ebner and
Stefan Hetzl and
Alexander Leitsch and
Giselle Reis and
Daniel Weller On the Generation of Quantified Lemmas 95--126
Tomá\vs Peitl and
Friedrich Slivovsky and
Stefan Szeider Long-Distance $Q$-Resolution with
Dependency Schemes . . . . . . . . . . . 127--155
Peter Lefanu Lumsdaine and
Nicolas Tabareau Preface: Special Issue on Homotopy Type
Theory and Univalent Foundations . . . . 157--158
Marc Bezem and
Thierry Coquand and
Simon Huber The Univalence Axiom in Cubical Sets . . 159--171
Simon Huber Canonicity for Cubical Type Theory . . . 173--210
Lars Birkedal and
Ale\vs Bizjak and
Ranald Clouston and
Hans Bugge Grathwohl and
Bas Spitters and
Andrea Vezzosi Guarded Cubical Type Theory . . . . . . 211--253
Guillaume Brunerie The James Construction and $ \pi_4
(\mathbb {S}^3) $ in Homotopy Type
Theory . . . . . . . . . . . . . . . . . 255--284
Benedikt Ahrens and
Ralph Matthes and
Anders Mörtberg From Signatures to Monads in UniMath . . 285--318
Mauricio Ayala-Rincón and
César Muñoz Selected Extended Papers of ITP 2017 . . 319--321
Xavier Allamigeon and
Ricardo D. Katz A Formalization of Convex Polyhedra
Based on the Simplex Method . . . . . . 323--345
Alexander Bentkamp and
Jasmin Christian Blanchette and
Dietrich Klakow A Formal Proof of the Expressiveness of
Deep Learning . . . . . . . . . . . . . 347--368
Frédéric Besson and
Sandrine Blazy and
Pierre Wilke CompCertS: a Memory-Aware Verified C
Compiler Using a Pointer as Integer
Semantics . . . . . . . . . . . . . . . 369--392
Yannick Forster and
Gert Smolka Call-by-Value Lambda Calculus as a Model
of Computation in Coq . . . . . . . . . 393--413
Dominik Kirst and
Gert Smolka Categoricity Results and Large Model
Constructions for Second-Order ZF in
Dependent Type Theory . . . . . . . . . 415--438
Andreas Lochbihler Effect Polymorphism in Higher-Order
Logic (Proof Pearl) . . . . . . . . . . 439--462
Adam Sandberg Ericsson and
Magnus O. Myreen and
Johannes Åman Pohjola A Verified Generational Garbage
Collector for CakeML . . . . . . . . . . 463--488
Yannick Zakowski and
David Cachera and
Delphine Demange and
Gustavo Petri and
David Pichardie and
Suresh Jagannathan and
Jan Vitek Verifying a Concurrent Garbage Collector
with a Rely-Guarantee Methodology . . . 489--515
Bohua Zhan Formalization of the Fundamental Group
in Untyped Set Theory Using Auto2 . . . 517--538
Jia Tao A PSpace Algorithm for Acyclic Epistemic
$ {\rm DL}(\mathcal {ALCS})5_m $ . . . . 539--555
Cezary Kaliszyk and
Karol P\kak Semantics of Mizar as an Isabelle Object
Logic . . . . . . . . . . . . . . . . . 557--595
Olaf Beyersdorff and
Joshua Blinkhorn and
Leroy Chew and
Renate Schmidt and
Martin Suda Reinterpreting Dependency Schemes:
Soundness Meets Incompleteness in DQBF 597--623
Dale Miller Mechanized Metatheory Revisited . . . . 625--665
Hing-Lun Chan and
Michael Norrish Classification of Finite Fields with
Applications . . . . . . . . . . . . . . 667--693
Lu\'ìs Cruz-Filipe and
Joao Marques-Silva and
Peter Schneider-Kamp Formally Verifying the Solution to the
Boolean Pythagorean Triples Problem . . 695--722
Wenxi Wang and
Harald Sòndergaard and
Peter J. Stuckey Wombit: a Portfolio Bit-Vector Solver
Using Word-Level Propagation . . . . . . 723--762
Mohammad Abdulaziz and
Lawrence C. Paulson An Isabelle/HOL Formalisation of Green's
Theorem . . . . . . . . . . . . . . . . 763--786
Li-Ming Li and
Zhi-Ping Shi and
Yong Guan and
Qian-Ying Zhang and
Yong-Dong Li Formalization of Geometric Algebra in
HOL Light . . . . . . . . . . . . . . . 787--808
Iliano Cervesato and
Maribel Fernández Preface to the Special Issue on
Linearity . . . . . . . . . . . . . . . 809--811
Patrick Baillot and
Gilles Barthe and
Ugo Dal Lago Implicit Computational Complexity of
Subrecursive Definitions and
Applications to Cryptographic Proofs . . 813--855
Quentin Heath and
Dale Miller A Proof Theory for Model Checking . . . 857--885
Ian Mackie Linear Numeral Systems . . . . . . . . . 887--909
Matteo Acclavio Proof Diagrams for Multiplicative Linear
Logic: Syntax and Semantics . . . . . . 911--939
Luca Paolini and
Mauro Piccolo and
Margherita Zorzi QPCF: Higher-Order Languages and Quantum
Circuits . . . . . . . . . . . . . . . . 941--966
Mohamed Yousri Mahmoud and
Amy P. Felty Formalization of Metatheory of the
Quipper Quantum Programming Language in
a Linear Logic . . . . . . . . . . . . . 967--1002
Clark Barrett and
Temesghen Kahsai Selected Extended Papers of NFM 2017:
Preface . . . . . . . . . . . . . . . . 1003--1004
Andrew Sogokon and
Paul B. Jackson and
Taylor T. Johnson Verifying Safety and Persistence in
Hybrid Systems Using Flowpipes and
Continuous Invariants . . . . . . . . . 1005--1029
Tommaso Dreossi and
Alexandre Donzé and
Sanjit A. Seshia Compositional Falsification of
Cyber-Physical Systems with Machine
Learning Components . . . . . . . . . . 1031--1053
Susmit Jha and
Tuhin Sahai and
Vasumathi Raman and
Alessandro Pinto and
Michael Francis Explaining AI Decisions Using Efficient
Methods for Learning Sparse Boolean
Formulae . . . . . . . . . . . . . . . . 1055--1075
Hadar Frenkel and
Orna Grumberg and
Sarai Sheinvald An Automata-Theoretic Approach to
Model-Checking Systems and
Specifications Over Infinite Data
Domains . . . . . . . . . . . . . . . . 1077--1101
Bernhard K. Aichernig and
Martin Tappler Efficient Active Automata Learning via
Mutation Testing . . . . . . . . . . . . 1103--1134
Cheng-Chao Huang and
Ming Xu and
Zhi-Bin Li A Conflict-Driven Solving Procedure for
Poly-Power Constraints . . . . . . . . . 1--20
Linh Anh Nguyen ExpTime Tableaux with Global Caching for
Hybrid PDL . . . . . . . . . . . . . . . 21--52
Christoph Benzmüller and
Dana S. Scott Automating Free Logic in HOL, with an
Experimental Application in Category
Theory . . . . . . . . . . . . . . . . . 53--72
Xingyuan Zhang and
Christian Urban and
Chunhan Wu Priority Inheritance Protocol Proved
Correct . . . . . . . . . . . . . . . . 73--95
Paula Chocron and
Pascal Fontaine and
Christophe Ringeissen Politeness and Combination Methods for
Theories with Bridging Functions . . . . 97--134
Marta Cialdea Mayer A Prover Dealing with Nominals, Binders,
Transitivity and Relation Hierarchies 135--165
Salvador Lucas Using Well-Founded Relations for Proving
Operational Termination . . . . . . . . 167--195
Peter Baumgartner and
Renate A. Schmidt Blocking and Other Enhancements for
Bottom-Up Model Generation Methods . . . 197--251
M. Echenim and
N. Peltier Combining Induction and Saturation-Based
Theorem Proving . . . . . . . . . . . . 253--294
Maximiliano Cristiá and
Gianfranco Rossi Solving Quantifier-Free First-Order
Constraints Over Finite Sets and Binary
Relations . . . . . . . . . . . . . . . 295--330
Wenda Li and
Lawrence C. Paulson Evaluating Winding Numbers and Counting
Complex Roots Through Cauchy Indices in
Isabelle/HOL . . . . . . . . . . . . . . 331--360
Armin Biere and
Cesare Tinelli and
Christoph Weidenbach Preface to the Special Issue on
Automated Reasoning Systems . . . . . . 361--362
Sebastiaan J. C. Joosten and
René Thiemann and
Akihisa Yamada A Verified Implementation of Algebraic
Numbers in Isabelle/HOL . . . . . . . . 363--389
Matt Kaufmann and
J. Strother Moore Limited Second--Order Functionality in a
First--Order Setting . . . . . . . . . . 391--422
Roberto Sebastiani and
Patrick Trentin OptiMathSAT: A Tool for Optimization
Modulo Theories . . . . . . . . . . . . 423--460
Cláudia Nalon and
Ullrich Hustadt and
Clare Dixon A Resolution--Based Theorem Prover for $
\mathsf {K}_n $: Architecture,
Refinements, Strategies and Experiments 461--484
Haniel Barbosa and
Jasmin Christian Blanchette and
Mathias Fleury and
Pascal Fontaine Scalable Fine--Grained Proofs for
Formula Processing . . . . . . . . . . . 485--510
Leonardo de Moura Preface: Selected Extended Papers of
CADE 2017 . . . . . . . . . . . . . . . 511--511
Peter Lammich Efficient Verified (UN)SAT Certificate
Checking . . . . . . . . . . . . . . . . 513--532
Marijn J. H. Heule and
Benjamin Kiesl and
Armin Biere Strong Extension--Free Proof Systems . . 533--554
Gadi Tellez and
James Brotherston Automatically Verifying Temporal
Properties of Pointer Programs with
Cyclic Proof . . . . . . . . . . . . . . 555--578
Maria Paola Bonacina and
Stéphane Graham-Lengrand and
Natarajan Shankar Conflict-Driven Satisfiability for
Theory Combination: Transition System
and Completeness . . . . . . . . . . . . 579--609
Andreas Teucke and
Christoph Weidenbach SPASS-AR: A First--Order Theorem Prover
Based on Approximation--Refinement into
the Monadic Shallow Linear Fragment . . 611--640
Lorenzo Gheri and
Andrei Popescu A Formalized General Theory of Syntax
with Bindings: Extended Version . . . . 641--675
Siddhartha Gadgil Homogeneous Length Functions on Groups:
Intertwined Computer and Human Proofs 677--688
G. I. Moghaddam and
R. Padmanabhan and
Yang Zhang Automated Reasoning with Power Maps . . 689--697
Jose Divasón and
Sebastiaan J. C. Joosten and
René Thiemann and
Akihisa Yamada A Verified Implementation of the
Berlekamp--Zassenhaus Factorization
Algorithm . . . . . . . . . . . . . . . 699--735
Mnacho Echenim and
Hervé Guiol and
Nicolas Peltier Formalizing the Cox--Ross--Rubinstein
Pricing of European Derivatives in
Isabelle/HOL . . . . . . . . . . . . . . 737--765
Ricardo Peña An Assertional Proof of Red--Black Trees
Using Dafny . . . . . . . . . . . . . . 767--791
Jeremy Avigad and
Assia Mahboubi Preface: Selected Extended Papers from
Interactive Theorem Proving 2018 . . . . 793--794
Christian Doczkal and
Damien Pous Graph Theory in Coq: Minors, Treewidth,
and Isomorphisms . . . . . . . . . . . . 795--825
René Thiemann and
Ralph Bottesch and
Jose Divasón and
Max W. Haslbeck and
Sebastiaan J. C. Joosten and
Akihisa Yamada Formalizing the LLL Basis Reduction
Algorithm and the LLL Factorization
Algorithm in Isabelle/HOL . . . . . . . 827--856
Matthew L. Daggitt and
Ran Zmigrod and
Timothy G. Griffin A Relaxation of Üresin and Dubois'
Asynchronous Fixed--Point Theory in Agda 857--877
Manuel Eberl and
Max W. Haslbeck and
Tobias Nipkow Verified Analysis of Random Binary Tree
Structures . . . . . . . . . . . . . . . 879--910
Hira Taqdees Syeda and
Gerwin Klein Formal Reasoning Under Cached Address
Translation . . . . . . . . . . . . . . 911--945
Matthieu Sozeau and
Abhishek Anand and
Simon Boulier and
Cyril Cohen and
Yannick Forster and
Fabian Kunze and
Gregory Malecha and
Nicolas Tabareau and
Théo Winterhalter The MetaCoq Project . . . . . . . . . . 947--999
Guillaume Burel and
Guillaume Bury and
Raphaël Cauderlier and
David Delahaye and
Pierre Halmagrand and
Olivier Hermant First-Order Automated Reasoning with
Theories: When Deduction Modulo Theory
Meets Practice . . . . . . . . . . . . . 1001--1050
Ákos Hajdu and
Zoltán Micskei Efficient Strategies for CEGAR-Based
Model Checking . . . . . . . . . . . . . 1051--1091
Clemens Ballarin Exploring the Structure of an Algebra
Text with Locales . . . . . . . . . . . 1093--1121
Reynald Affeldt and
Jacques Garrigue and
Takafumi Saikawa A Library for Formalization of Linear
Error-Correcting Codes . . . . . . . . . 1123--1164
Didier Galmiche and
Stephan Schulz and
Roberto Sebastiani Preface: Special Issue of Selected
Extended Papers from IJCAR 2018 . . . . 1165--1167
Anders Schlichtkrull and
Jasmin Blanchette and
Dmitriy Traytel and
Uwe Waldmann Formalizing Bachmair and Ganzinger's
Ordered Resolution Prover . . . . . . . 1169--1195
Dominique Larchey-Wendling Constructive Decision via
Redundancy-Free Proof-Search . . . . . . 1197--1219
Anupam Das From QBFs to MALL and Back via Focussing 1221--1245
Benjamin Kiesl and
Adrián Rebola-Pardo and
Marijn J. H. Heule and
Armin Biere Simulating Strong Practical Proof
Systems with Extended Resolution . . . . 1247--1267
Marcelo Finger and
Sandro Preto Probably Partially True: Satisfiability
for \Lukasiewicz Infinitely Valued
Probabilistic Logic and Related Topics 1269--1286
Oskar Abrahamsson and
Son Ho and
Hrutvik Kanabar and
Ramana Kumar and
Magnus O. Myreen and
Michael Norrish and
Yong Kiam Tan Proof-Producing Synthesis of CakeML from
Monadic HOL Functions . . . . . . . . . 1287--1306
Sylvain Conchon and
David Declerck and
Fatiha Za\"\idi Parameterized Model Checking on the TSO
Weak Memory Model . . . . . . . . . . . 1307--1330
Dirk Beyer and
Marieke Huisman Selected and Extended Papers from TACAS
2018: Preface . . . . . . . . . . . . . 1331--1332
Kshitij Bansal and
Eric Koskinen and
Omer Tripp Synthesizing Precise and Useful
Commutativity Conditions . . . . . . . . 1333--1359
Randal E. Bryant Chain Reduction for Binary and
Zero-Suppressed Decision Diagrams . . . 1361--1391
Adrien Champion and
Tomoya Chiba and
Naoki Kobayashi and
Ryosuke Sato ICE-Based Refinement Type Discovery for
Higher-Order Functional Programs . . . . 1393--1418
Peter Chini and
Roland Meyer and
Prakash Saivasan Fine-Grained Complexity of Safety
Verification . . . . . . . . . . . . . . 1419--1444
Gabriele Costa and
Letterio Galletta and
Pierpaolo Degano and
David Basin and
Chiara Bodei Natural Projection as Partial Model
Checking . . . . . . . . . . . . . . . . 1445--1481
Arnd Hartmanns and
Sebastian Junges and
Joost-Pieter Katoen and
Tim Quatmann Multi-cost Bounded Tradeoff Analysis in
MDP . . . . . . . . . . . . . . . . . . 1483--1522
Daniel Neider and
P. Madhusudan and
Shambwaditya Saha and
Pranav Garg and
Daejun Park A Learning-Based Approach to
Synthesizing Invariants for Incomplete
Verification Engines . . . . . . . . . . 1523--1552
Ullrich Hustadt and
Ana Ozaki and
Clare Dixon Theorem Proving for Pointwise Metric
Temporal Logic Over the Naturals via
Translations . . . . . . . . . . . . . . 1553--1610
Salvador Lucas and
José Meseguer and
Raúl Gutiérrez The $2$D Dependency Pair Framework for
Conditional Rewrite Systems--- Part II:
Advanced Processors and Implementation
Techniques . . . . . . . . . . . . . . . 1611--1662
R. Alonderis and
R. Pliu\vskevi\vcius and
A. Pliu\vskevi\vcien\.e and
H. Giedra Loop-Type Sequent Calculi for Temporal
Logic . . . . . . . . . . . . . . . . . 1663--1684
Gilles Barthe and
Gustavo Betarte and
Juan Diego Campo and
Carlos Luna and
David Pichardie System-Level Non-interference of
Constant-Time Cryptography. Part II:
Verified Static Analysis and Stealth
Memory . . . . . . . . . . . . . . . . . 1685--1729
Yong Guan and
Jingzhi Zhang and
Yongdong Li Formalization of Euler--Lagrange
Equation Set Based on Variational
Calculus in HOL Light . . . . . . . . . 1--29
Danijela Simi\'c and
Filip Mari\'c and
Pierre Boutry Formalization of the Poincaré Disc Model
of Hyperbolic Geometry . . . . . . . . . 31--73
Guillaume Ambal and
Sergue\"\i Lenglet and
Alan Schmitt HO$ \pi $ in Coq . . . . . . . . . . . . 75--124
Olaf Beyersdorff and
Joshua Blinkhorn and
Meena Mahajan Building Strategies into QBF Proofs . . 125--154
Jasmin Blanchette Message from the New Editor-in-Chief . . 155--155
Dario Cattaruzza and
Alessandro Abate and
Daniel Kroening Unbounded-Time Safety Verification of
Guarded LTI Models with Inputs by
Abstract Acceleration . . . . . . . . . 157--203
Hing Lun Chan and
Michael Norrish Mechanisation of the AKS Algorithm . . . 205--256
Thibault Gauthier and
Cezary Kaliszyk and
Michael Norrish TacticToe: Learning to Prove with
Tactics . . . . . . . . . . . . . . . . 257--286
Michael Färber and
Cezary Kaliszyk and
Josef Urban Machine Learning Guidance for Connection
Tableaux . . . . . . . . . . . . . . . . 287--320
Andrei Popescu and
Peter Lammich and
Ping Hou CoCon: A Conference Management System
with Formally Verified Document
Confidentiality . . . . . . . . . . . . 321--356
Marco Voigt Decidable $ \exists^* \forall^* $
First-Order Fragments of Linear Rational
Arithmetic with Uninterpreted Predicates 357--423
Silvio Ghilardi and
Elena Pagani Higher-Order Quantifier Elimination,
Counter Simulations and Fault-Tolerant
Systems . . . . . . . . . . . . . . . . 425--460
Dirk Beyer and
Matthias Dangl and
Philipp Wendler Correction to: A Unifying View on
SMT-Based Software Verification . . . . 461--461
Maximiliano Cristiá and
Gianfranco Rossi Automated Proof of Bell--LaPadula
Security Properties . . . . . . . . . . 463--478
Véronique Cortier and
Stéphanie Delaune and
Vaishnavi Sundararajan A Decidable Class of Security Protocols
for Both Reachability and Equivalence
Properties . . . . . . . . . . . . . . . 479--520
D. Butler and
A. Lochbihler and
A. Gascón Formalising $ \Sigma $-Protocols and
Commitment Schemes Using CryptHOL . . . 521--567
Zhé Hóu and
David Sanan and
Jin Song Dong An Isabelle/HOL Formalisation of the
SPARC Instruction Set Architecture and
the TSO Memory Model . . . . . . . . . . 569--598
David M. Cerna and
Alexander Leitsch and
Anela Lolic Schematic Refutations of Formula
Schemata . . . . . . . . . . . . . . . . 599--645
Christoph Wernhard Craig Interpolation with Clausal
First-Order Tableaux . . . . . . . . . . 647--690
Anthony Bordg and
Hanna Lachnitt and
Yijun He Certified Quantum Computation in
Isabelle/HOL . . . . . . . . . . . . . . 691--709
Xicheng Peng and
Qihang Chen and
Mao Chen Automated Discovery of Geometric
Theorems Based on Vector Equations . . . 711--726
Mauro Vallati and
Luká\vs Chrpa and
Frank Hutter On the Importance of Domain Model
Configuration for Automated Planning
Engines . . . . . . . . . . . . . . . . 727--773
Alexander Steen and
Christoph Benzmüller Extensional Higher-Order Paramodulation
in Leo-III . . . . . . . . . . . . . . . 775--807
Maximiliano Cristiá and
Gianfranco Rossi Automated Reasoning with Restricted
Intensional Sets . . . . . . . . . . . . 809--890
Pascal Fontaine Preface: Special Issue of Selected
Extended Papers of CADE 2019 . . . . . . 891--892
Alexander Bentkamp and
Jasmin Blanchette and
Uwe Waldmann Superposition with Lambdas . . . . . . . 893--940
Diego Calvanese and
Silvio Ghilardi and
Andrey Rivkin Model Completeness, Uniform Interpolants
and Superposition Calculus . . . . . . . 941--969
Vojt\vech Havlena and
Luká\vs Holík and
Tomá\vs Vojnar Automata Terms in a Lazy WS$k$S Decision
Procedure . . . . . . . . . . . . . . . 971--999
Aina Niemetz and
Mathias Preiner and
Cesare Tinelli Towards Satisfiability Modulo Parametric
Bit-vectors . . . . . . . . . . . . . . 1001--1025
Andrei Popescu and
Dmitriy Traytel Distilling the Requirements of Gödel's
Incompleteness Theorems with a Proof
Assistant . . . . . . . . . . . . . . . 1027--1070
Patrick Trentin and
Roberto Sebastiani Optimization Modulo the Theories of
Signed Bit-Vectors and Floating-Point
Numbers . . . . . . . . . . . . . . . . 1071--1096
Koen Claessen and
Ann Lillieström Handling Transitive Relations in
First-Order Automated Reasoning . . . . 1097--1124
Maximiliano Cristiá and
Gianfranco Rossi An Automatically Verified Prototype of
the Tokeneer ID Station Specification 1125--1151
Wilfried Sieg and
Farzaneh Derakhshan Human-Centered Automated Proof Search 1153--1190
Salvador Lucas Derivational Complexity and
Context-Sensitive Rewriting . . . . . . 1191--1229
Thaynara Arielly de Lima and
André Luiz Galdino and
Mauricio Ayala-Rincón Formalization of Ring Theory in PVS . . 1231--1263
Michael Kohlhase and
Florian Rabe Experiences from Exporting Major Proof
Assistant Libraries . . . . . . . . . . 1265--1298
Sarah Sigley and
Olaf Beyersdorff Proof Complexity of Modal Resolution . . 1--41
Maria Paola Bonacina and
Stéphane Graham-Lengrand and
Natarajan Shankar Conflict-Driven Satisfiability for
Theory Combination: Lemmas, Modules, and
Proofs . . . . . . . . . . . . . . . . . 43--91
Jonathan Julián Huerta y Munive and
Georg Struth Predicate Transformer Semantics for
Hybrid Systems . . . . . . . . . . . . . 93--139
Sadegh Dalvandi and
Brijesh Dongol and
Heike Wehrheim Integrating Owicki--Gries for C11-Style
Memory Models into Isabelle/HOL . . . . 141--171
André Platzer Correction to: Differential Dynamic
Logic for Hybrid Systems . . . . . . . . 173--173
Sylvie Boldo and
François Clément and
Micaela Mayero A Coq Formalization of Lebesgue
Integration of Nonnegative Functions . . 175--213
Robert Y. Lewis and
Minchao Wu A Bi-Directional Extensible Interface
Between Lean and Mathematica . . . . . . 215--238
Piotr Wojciechowski and
K. Subramani and
R. Chandrasekaran Analyzing Read-Once Cutting Plane Proofs
in Horn Systems . . . . . . . . . . . . 239--274
Nicolas Peltier and
Viorica Sofronie-Stokkermans Special Issue of Selected Extended
Papers of IJCAR 2020 . . . . . . . . . . 275--276
Joshua Brakensiek and
Marijn Heule and
David Narváez The Resolution of Keller's Conjecture 277--300
Franz Baader and
Deepak Kapur Deciding the Word Problem for Ground and
Strongly Shallow Identities w.r.t.
Extensional Symbols . . . . . . . . . . 301--329
Ying Sheng and
Yoni Zohar and
Clark Barrett Polite Combination of Algebraic
Datatypes . . . . . . . . . . . . . . . 331--355
Franz Baader and
Jakub Rydval Using Model Theory to Find Decidable and
Tractable Description Logics with
Concrete Domains . . . . . . . . . . . . 357--407
Diego Calvanese and
Silvio Ghilardi and
Andrey Rivkin Combination of Uniform Interpolants via
Beth Definability . . . . . . . . . . . 409--435
Maria Paola Bonacina Six Decades of Automated Reasoning:
Papers in Memory of Larry Wos . . . . . 437--438
Michael Beeson and
Maria Paola Bonacina and
Michael Kinyon and
Geoff Sutcliffe Larry Wos: Visions of Automated
Reasoning . . . . . . . . . . . . . . . 439--461
Maria Paola Bonacina Set of Support, Demodulation,
Paramodulation: a Historical Perspective 463--497
Uwe Waldmann and
Sophie Tourret and
Simon Robillard and
Jasmin Blanchette A Comprehensive Framework for Saturation
Theorem Proving . . . . . . . . . . . . 499--539
Petar Vukmirovi\'c and
Alexander Bentkamp and
Jasmin Blanchette and
Simon Cruanes and
Visa Nummelin and
Sophie Tourret Making Higher-Order Superposition Work 541--564
Robert Veroff A Wos Challenge Met . . . . . . . . . . 565--574
Sophie Tourret and
Christoph Weidenbach A Posthumous Contribution by Larry Wos:
Excerpts from an Unpublished Column . . 575--584
Andreas Lochbihler A Mechanized Proof of the Max--Flow
Min--Cut Theorem for Countable Networks
with Applications to Probability Theory 585--610
Anne Baanen and
Sander R. Dahmen and
Ashvni Narayanan and
Filippo A. E. Nuccio Mortarino Majno di Capriglio A Formalization of Dedekind Domains and
Class Groups of Global Fields . . . . . 611--637
Fabio Papacchini and
Cláudia Nalon and
Ullrich Hustadt and
Clare Dixon Local is Best: Efficient Reductions to
Modal Logic K . . . . . . . . . . . . . 639--666
Akihisa Yamada Tuple Interpretations for Termination of
Term Rewriting . . . . . . . . . . . . . 667--688
Predrag Jani\vci\'c and
Julien Narboux Theorem Proving as Constraint Solving
with Coherent Logic . . . . . . . . . . 689--746
David J. Pearce and
Mark Utting and
Lindsay Groves Verifying Whiley Programs with Boogie 747--803
Joshua Meyers and
David I. Spivak and
Ryan Wisnesky Fast Left Kan Extensions Using the Chase 805--844
Dennis de Champeaux Faster Linear Unification Algorithm . . 845--860
Nuno Macedo and
Julien Brunel and
David Chemouil and
Alcino Cunha Pardinus: a Temporal Relational Model
Finder . . . . . . . . . . . . . . . . . 861--904
Mallku Soldevila and
Beta Ziliani and
Bruno Silvestre From Specification to Testing: Semantics
Engineering for Lua 5.2 . . . . . . . . 905--952
Richard Schmoetten and
Jake E. Palmer and
Jacques D. Fleuriot Towards Formalising Schutz' Axioms for
Minkowski Spacetime in Isabelle/HOL . . 953--988
Wilmer Ricciotti and
James Cheney A Formalization of SQL with Nulls . . . 989--1030
Thiago Mendonça Ferreira Ramos and
Ariane Alves Almeida and
Mauricio Ayala-Rincón Formalization of the Computational
Theory of a Turing Complete Functional
Language Model . . . . . . . . . . . . . 1031--1063
Jose Divasón and
René Thiemann A Formalization of the Smith Normal Form
in Higher--Order Logic . . . . . . . . . 1065--1095
Jose Divasón and
René Thiemann Correction to: A Formalization of the
Smith Normal Form in Higher--Order Logic 1097--1097
Fabio Papacchini and
Cláudia Nalon and
Ullrich Hustadt and
Clare Dixon Correction to: Local is Best: Efficient
Reductions to Modal Logic K . . . . . . 1099--1099
Simon Roßkopf and
Tobias Nipkow A Formalization and Proof Checker for
Isabelle's Metalogic . . . . . . . . . . ??
Chelsea Edmonds and
Angeliki Koutsoukou-Argyraki and
Lawrence C. Paulson Formalising Szemerédi's Regularity Lemma
and Roth's Theorem on Arithmetic
Progressions in Isabelle/HOL . . . . . . ??
Guido Fiorino Linear Depth Deduction with Subformula
Property for Intuitionistic Epistemic
Logic . . . . . . . . . . . . . . . . . ??
Qinshi Wang and
Andrew W. Appel A Solver for Arrays with Concatenation ??
Pedro Quaresma and
Pierluigi Graziani Measuring the Readability of Geometric
Proofs: The Area Method Case . . . . . . ??
Maria Paola Bonacina and
Sarah Winkler Semantically-Guided Goal-Sensitive
Reasoning: Decision Procedures and the
Koala Prover . . . . . . . . . . . . . . ??
Alvaro Velasquez and
Ismail Alkhouri and
K. Subramani and
Piotr Wojciechowski and
George Atia Optimal Deterministic Controller
Synthesis from Steady-State
Distributions . . . . . . . . . . . . . ??
Andrew W. Appel and
Xavier Leroy Efficient Extensional Binary Tries . . . ??
Richard Schmoetten and
Jake E. Palmer and
Jacques D. Fleuriot Correction: Towards Formalising Schutz'
Axioms for Minkowski Spacetime in
Isabelle/HOL . . . . . . . . . . . . . . ??
Alexander Bentkamp and
Jasmin Blanchette and
Sophie Tourret and
Petar Vukmirovi\'c Superposition for Higher-Order Logic . . ??
Mak Andrlon Finding Normal Binary Floating-Point
Factors Efficiently . . . . . . . . . . ??
Aaron A. Windsor Computer-Aided Constructions of
Commafree Codes . . . . . . . . . . . . ??
Dominik Kirst and
Marc Hermes Synthetic Undecidability and
Incompleteness of First-Order Axiom
Systems in Coq . . . . . . . . . . . . . ??
Aart Middeldorp and
Alexander Lochmann and
Fabian Mitterwallner First-Order Theory of Rewriting for
Linear Variable-Separated Rewrite
Systems: Automation, Formalization,
Certification . . . . . . . . . . . . . ??
Emre Yolcu and
Scott Aaronson and
Marijn J. H. Heule An Automated Approach to the Collatz
Conjecture . . . . . . . . . . . . . . . ??
Gabriel Ebner and
Jasmin Blanchette and
Sophie Tourret Unifying Splitting . . . . . . . . . . . ??
Maximiliano Cristiá and
Guido De Luca and
Carlos Luna An Automatically Verified Prototype of
the Android Permissions System . . . . . ??
Oliver Nash Engel's Theorem in Mathlib . . . . . . . ??
Alessandro Abate and
Haniel Barbosa and
Clark Barrett and
Cristina David and
Pascal Kesseli and
Daniel Kroening and
Elizabeth Polgreen and
Andrew Reynolds and
Cesare Tinelli Synthesising Programs with Non-trivial
Constants . . . . . . . . . . . . . . . ??
Cezary Kaliszyk and
Karol P\kak Combining Higher-Order Logic with Set
Theory Formalizations . . . . . . . . . ??
Luís Cruz-Filipe and
Fabrizio Montesi and
Marco Peressotti A Formal Theory of Choreographic
Programming . . . . . . . . . . . . . . ??
Hendrik Leidinger and
Christoph Weidenbach SCL(EQ): SCL for First--Order Logic with
Equality . . . . . . . . . . . . . . . . ??
Andrei Popescu Rensets and Renaming-Based Recursion for
Syntax with Bindings Extended Version ??
Christian Urban POSIX Lexing with Derivatives of Regular
Expressions . . . . . . . . . . . . . . ??
\vSt\vepán Holub and
Martin Ra\vska and
\vSt\vepán Starosta Binary Codes that do not Preserve
Primitivity . . . . . . . . . . . . . . ??
Yun-Rong Luo and
Che Cheng and
Jie-Hong R. Jiang A Resolution Proof System for Dependency
Stochastic Boolean Satisfiability . . . ??
Anupam Das and
Marianna Girlando Cyclic Hypersequent System for
Transitive Closure Logic . . . . . . . . ??
Reynald Affeldt and
Cyril Cohen Measure Construction by Extension in
Dependent Type Theory with Application
to Integration . . . . . . . . . . . . . ??
Marco Maggesi and
Cosimo Perini Brogi Mechanising Gödel--Löb Provability Logic
in HOL Light . . . . . . . . . . . . . . ??
Mnacho Echenim and
Nicolas Peltier A Proof Procedure for Separation Logic
with Inductive Definitions and Data . . ??
Joseph E. Reeves and
Marijn J. H. Heule and
Randal E. Bryant Preprocessing of Propagation Redundant
Clauses . . . . . . . . . . . . . . . . ??
Ying Sheng and
Andres Nötzli and
Andrew Reynolds and
Yoni Zohar and
David Dill and
Wolfgang Grieskamp and
Junkil Park and
Shaz Qadeer and
Clark Barrett and
Cesare Tinelli Reasoning About Vectors: Satisfiability
Modulo a Theory of Sequences . . . . . . ??
Érik Martin-Dorel and
Guillaume Melquiond and
Pierre Roux Enabling Floating-Point Arithmetic in
the Coq Proof Assistant . . . . . . . . ??
Ying Sheng and
Yoni Zohar and
Christophe Ringeissen and
Andrew Reynolds and
Clark Barrett and
Cesare Tinelli Combining Stable Infiniteness and
(Strong) Politeness . . . . . . . . . . ??
Benjamin Böhm and
Olaf Beyersdorff Lower Bounds for QCDCL via Formula Gauge ??
Philipp G. Haselwarter and
Andrej Bauer Finitary Type Theories With and Without
Contexts . . . . . . . . . . . . . . . . ??
Andrzej Indrzejczak Bisequent Calculus for Four-Valued
Quasi-Relevant Logics: Cut Elimination
and Interpolation . . . . . . . . . . . ??
Xicheng Peng and
Jingzhong Zhang and
Mao Chen and
Sannyuya Liu Self-evident Automated Geometric Theorem
Proving Based on Complex Number Identity ??
Sen Zheng and
Renate A. Schmidt Saturation-Based Boolean Conjunctive
Query Answering and Rewriting for the
Guarded Quantification Fragments . . . . ??
Florian Faissole Formally-Verified Round-Off Error
Analysis of Runge--Kutta Methods . . . . ??
Mnacho Echenim and
Mehdi Mhalla A Formalization of the CHSH Inequality
and Tsirelson's Upper-bound in
Isabelle/HOL . . . . . . . . . . . . . . ??
David Braun and
Nicolas Magaud and
Pascal Schreck A Matroid-Based Automatic Prover and Coq
Proof Generator for Projective Incidence
Geometry . . . . . . . . . . . . . . . . ??
Étienne Payet Non-termination in Term Rewriting and
Logic Programming . . . . . . . . . . . ??
Benjamin Böhm and
Tomá\vs Peitl and
Olaf Beyersdorff Should Decisions in QCDCL Follow Prefix
Order? . . . . . . . . . . . . . . . . . ??
Luca Geatti and
Nicola Gigante and
Angelo Montanari and
Gabriele Venturato SAT Meets Tableaux for Linear Temporal
Logic Satisfiability . . . . . . . . . . ??
Dominic Steinhöfel and
Reiner Hähnle Schematic Program Proofs with Abstract
Execution . . . . . . . . . . . . . . . ??
Michael Bernreiter and
Anela Lolic and
Jan Maly and
Stefan Woltran Sequent Calculi for Choice Logics . . . ??
Filip Smola and
Jacques D. Fleuriot Linear Resources in Isabelle/HOL . . . . ??
Lei Li and
Zongkai Yang and
Mao Chen and
Xicheng Peng and
Jianwen Sun and
Zhonghua Yan and
Sannyuya Liu Automated Generation of Geometry Proof
Problems Based on Point Geometry
Identity . . . . . . . . . . . . . . . . ??
Tobias Nipkow Gale--Shapley Verified . . . . . . . . . ??
Camillo Fiorentini and
Mauro Ferrari General Clauses for SAT--Based Proof
Search in Intuitionistic Propositional
Logic . . . . . . . . . . . . . . . . . ??
Peter Lammich Refinement of Parallel Algorithms Down
to LLVM: Applied to Practically
Efficient Parallel Sorting . . . . . . . ??
Asta Halkjær From and
Frederik Krogsdal Jacobsen Verifying a Sequent Calculus Prover for
First-Order Logic with Functions in
Isabelle/HOL . . . . . . . . . . . . . . ??
Abhimanyu Choudhury and
Meena Mahajan Dependency Schemes in CDCL--Based QBF
Solving: a Proof-Theoretic Study . . . . ??
Guy Amir and
Osher Maayan and
Tom Zelazny and
Guy Katz and
Michael Schapira Verifying the Generalization of Deep
Learning to Out-of-Distribution Domains ??
Zhongye Wang and
Qinxiang Cao and
Yichen Tao Verifying Programs with Logic and
Extended Proof Rules: Deep Embedding vs.
Shallow Embedding . . . . . . . . . . . ??
Jason Gross and
Andres Erbsen and
Jade Philipoom and
Rajashree Agrawal and
Adam Chlipala Towards a Scalable Proof Engine: a
Performant Prototype Rewriting Primitive
for Coq . . . . . . . . . . . . . . . . ??