Muutke küpsiste eelistusi

E-raamat: Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II

  • Formaat - EPUB+DRM
  • Hind: 80,26 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods).





The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics:

Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics

Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools

*The conference was held virtually due to the COVID-19 pandemic.





Chapter A Fast Verified Liveness Analysis in SSA Form is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com.
Interactive Theorem Proving/ HOL.- Competing inheritance paths in
dependent type theory: a case study in functional analysis.- A Lean tactic
for normalising ring expressions with exponents (short paper).- Practical
proof search for Coq by type inhabitation.- Quotients of Bounded Natural
Functors.- Trakhtenbrots Theorem in Coq.- Deep Generation of Coq Lemma Names
Using Elaborated Terms.- Extensible Extraction of Efficient Imperative
Programs with Foreign Functions, Manually Managed Memory, and Proofs.-
Validating Mathematical Structures.- Teaching Automated Theorem Proving by
Example: PyRes 1.2 (system description).- Beyond Notations: Hygienic Macro
Expansion for Theorem Proving Languages.- Formalizations.- Formalizing the
Face Lattice of Polyhedra.- Algebraically Closed Fields in Isabelle/HOL.-
Formalization of Forcing in Isabelle/ZF.- Reasoning about Algebraic
Structures with Implicit Carriers in Isabelle/HOL.- Formal Proof of the Group
Law for Edwards Elliptic Curves.- Verifying Farad_zev-Read type Isomorph-Free
Exhaustive Generation.- Verification.- Verified Approximation Algorithms.-
Efficient Verified Implementation of Introsort and Pdqsort.- A Fast Verified
Liveness Analysis in SSA form.- Verification of Closest Pair of Points
Algorithms.- Reasoning Systems and Tools.- A Polymorphic Vampire (short
paper).- N-PAT: A Nested Model-Checker (system description).- HYPNO: Theorem
Proving with Hypersequent Calculi for Non-Normal Modal Logics (system
description).- Implementing superposition in iProver (system description).-
Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system
description).- Make E Smart Again.- Automatically Proving and Disproving
Feasibility Conditions.- µ-term: Verify Termination Properties Automatically
(system description).- ENIGMA Anonymous: Symbol-Independent Inference Guiding
Machine (system description).- The Imandra Automated Reasoning System (system
description).- A Programmers Text Editor for a Logical Theory: The SUMOjEdit
Editor (system description).- Sequoia: a playground for logicians (system
description).- Prolog Technology Reinforcement Learning Prover (system
description).