24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013 ; Maria Paola Bonacina (ed.).
وضعیت نشر و پخش و غیره
محل نشرو پخش و غیره
Heidelberg
نام ناشر، پخش کننده و غيره
Springer
تاریخ نشرو بخش و غیره
2013
مشخصات ظاهری
نام خاص و کميت اثر
466 Seiten : Illustrationen
فروست
عنوان فروست
Lecture notes in computer science, 7898 : Lecture notes in artificial intelligence
یادداشتهای مربوط به مندرجات
متن يادداشت
One Logic to Use Them All.- The Tree Width of Separation Logic with Recursive Definitions.- Hierarchic Superposition with Weak Abstraction.- Completeness and Decidability Results for First-Order Clauses with Indices.- A Proof Procedure for Hybrid Logic with Binders, Transitivity andRelation Hierarchies.- Tractable Inference Systems: An Extension with a Deducibility Predicate.- Computing Tiny Clause Normal Forms.- System Description: E-KRHyper 1.4 Extensions for Unique Names and Description Logic.- Analysing Vote Counting Algorithms via Logic: And Its Applicationto the CADE Election Scheme.- Automated Reasoning, Fast and Slow.- Foundational Proof Certificates in First-Order Logic.- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition.- dReal: An SMT Solver for Nonlinear Theories over the Reals.- Solving Difference Constraints over Modular Arithmetic.- Asymmetric Unification: A New Unification Paradigm for CryptographicProtocol Analysis.- Hierarchical Combination.- PRocH: Proof Reconstruction for HOL Light.- An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description.- Towards Modularly Comparing Programs Using Automated Theorem Provers.- Reuse in Software Verification by Abstract Method Calls.- Dynamic Logic with Trace Semantics.- Temporalizing Ontology-Based Data Access.- Verifying Refutations with Extended Resolution.- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems.- Quantifier Instantiation Techniques for Finite Model Finding in SMT.- Automating Inductive Proofs Using Theory Exploration.- E-MaLeS 1.1.- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism.- Propositional Temporal Proving with Reductions to a SAT Problem.- InKreSAT: Modal Reasoning via Incremental Reduction to SAT.- bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR.- The 481 Ways to Split a Clause and Deal with Propositional Variables.
موضوع (اسم عام یاعبارت اسمی عام)
موضوع مستند نشده
Automatisches Beweisverfahren
موضوع مستند نشده
DÉDUCTION + DÉMONSTRATION DE THÉORÈMES (INTELLIGENCE ARTIFICIELLE)
موضوع مستند نشده
DEDUKTION + BEWEISEN VON THEOREMEN (KÜNSTLICHE INTELLIGENZ)
نام شخص به منزله سر شناسه - (مسئولیت معنوی درجه اول )
مستند نام اشخاص تاييد نشده
24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013 ; Maria Paola Bonacina (ed.).