Automated reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings.: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings. Part II (2020)

• Record Type: Book
• Other Titles: IJCAR 2020
• Further Information: Note: Nicolas Peltier, Viorica Sofronie-Stokkermans (eds.).
• Other Names: Peltier, Nicholas; Sofronie-Stokkermans, Viorica; IJCAR (Conference), 10th
• Contents: 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 Programmer s 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).
• Publisher Details: Cham : Springer
• Publication Date: 2020
• Extent: 1 online resource (521 p.)
• Subjects: 511.3/6028563; Automatic theorem proving -- Congresses; Computer logic -- Congresses; Artificial intelligence; Computer programming / software development; Software Engineering; Programming & scripting languages: general; Mathematical theory of computation; Computers -- Intelligence (AI) & Semantics; Computers -- Programming -- General; Computers -- Software Development & Engineering -- General; Computers -- Programming Languages -- General; Mathematics -- Logic; Automatic theorem proving; Computer logic; Electronic books; Electronic books; Conference papers and proceedings
• Languages: English
• ISBNs: 9783030510541; 3030510549; 9783030510541
• Related ISBNs: 9783030510534
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.