Atjaunināt sīkdatņu piekrišanu

Automated Deduction CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings [Mīkstie vāki]

Edited by , Edited by
  • Formāts: Paperback / softback, 724 pages, height x width: 235x155 mm, 90 Illustrations, black and white; XX, 724 p. 90 illus., 1 Paperback / softback
  • Sērija : Lecture Notes in Artificial Intelligence 15943
  • Izdošanas datums: 27-Aug-2025
  • Izdevniecība: Springer International Publishing AG
  • ISBN-10: 3031999835
  • ISBN-13: 9783031999833
Citas grāmatas par šo tēmu:
  • Mīkstie vāki
  • Cena: 37,98 €*
  • * ši ir gala cena, t.i., netiek piemērotas nekādas papildus atlaides
  • Standarta cena: 44,69 €
  • Ietaupiet 15%
  • Grāmatu piegādes laiks ir 3-4 nedēļas, ja grāmata ir uz vietas izdevniecības noliktavā. Ja izdevējam nepieciešams publicēt jaunu tirāžu, grāmatas piegāde var aizkavēties.
  • Daudzums:
  • Ielikt grozā
  • Piegādes laiks - 4-6 nedēļas
  • Pievienot vēlmju sarakstam
Automated Deduction CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, ProceedingsPalielināt
  • Formāts: Paperback / softback, 724 pages, height x width: 235x155 mm, 90 Illustrations, black and white; XX, 724 p. 90 illus., 1 Paperback / softback
  • Sērija : Lecture Notes in Artificial Intelligence 15943
  • Izdošanas datums: 27-Aug-2025
  • Izdevniecība: Springer International Publishing AG
  • ISBN-10: 3031999835
  • ISBN-13: 9783031999833
Citas grāmatas par šo tēmu:
Permanent link: https://www.kriso.lv/db/9783031999833.html
This open access book constitutes the proceedings of the 30th International Conference on Automated Deduction, CADE 30, which took place in Stuttgart, Germany, during July 2025. 



CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. 



The 33 full papers and 4 short papers included in these proceedings were carefully reviewed and selected from 87 submissions. They were organized in topical sections on SMT; rewriting; formalizations in Isabelle/HOL; calculi; machine learning for automated deduction; model checking and quantifier elimination; saturation; equational reasoning; non-classical logics; and SAT.
.- Invited Talks.
.- A Decade of Lean: Advancing Proof Automation for Mathematics and Software
Verification.
.- Taming Infinity for Verification in First-Order Logic.
.- Choose Your Proofs: Commutativity and Symmetry for Smarter Reasoning.
.- SMT.
.- Being polite is not enough (and other limits of theory combination).
.- On Symbol Elimination and Uniform Interpolation in Theory Extensions.
.- Whats Decidable About Arrays With Sums?
.- Cazamariposas: Automated Instability Debugging in SMT-based Program
Verification.
.- Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.
.- More is Less: Adding Polynomials for Faster Explanations in NLSAT.
.- Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories.
.- SMT and Functional Equation Solving over the Reals: Challenges from the
IMO.
.- Rewriting.
.- Lexicographic Combination of Reduction Pairs.
.- Confluence of Almost Parallel-Closed Generalized Term Rewriting Systems.
.- The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting.
.- Sort-Based Confluence Criteria for Non-Left-Linear
Higher-Order Rewriting.
.- Formalizations in Isabelle/HOL.
.- Verified Path Indexing.
.- Simplified and Verified: A Second Look at a Proof-Producing Union-Find
Algorithm.
.- Faithful Logic Embeddings in HOL Deep and Shallow.
.- A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered
Resolution.
.- Calculi.
.- Interoperability of Proof systems with SC-TPTP (System Description) .
.- Cut Elimination for Negative Free Logics with Definite Descriptions.
.- From Modal Sequent Calculi to Modal Resolution.
.- A Fresh Inductive Approach to Useful Call-by-Value.
.- Machine Learning for Automated Deduction.
.- Efficient Neural Clause-Selection Reinforcement.
.- Learning Conjecturing from Scratch.
.- Model Checking and Quantifier Elimination.
.- A Theorem Prover Based Approach for SAT-Based Model
Checking Certification.
.- Infinite State Model Checking by Learning Transitive Relations.
.- Relatively Complete and Efficient Partial Quantifier Elimination.
.- Saturation.
.- Computing Witnesses Using the SCAN Algorithm.
.- Partial Redundancy in Saturation.
.- Term Ordering Diagrams.
.- Equational Reasoning.
.- Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL.
.- Computing Ground Congruence Classes.
.- Anti-pattern templates.
.- Equational Reasoning Modulo Commutativity in Languages with Binders.
.- Non-Classical Logics.
.- Uniform Interpolation and Forgetting for Large-Scale Ontologies
with Application to Semantic Difference in SNOMED CT.
.- Concrete Domains Meet Expressive Cardinality Restrictions in Description
Logics.
.- A Real-Analytic Approach to Differential-Algebraic Dynamic Logic.
.- SAT.
.- Entailment vs. Verification for Partial-assignment Satisfiability
and Enumeration.
.- Unfolding Boxes with Local Constraints.