IJCAR 2020: 10TH INTERNATIONAL JOINT CONFERENCE ON AUTOMATED REASONING

A
Affeldt, Reynald	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
Aitken, David	The Imandra Automated Reasoning System (system description)
Allamigeon, Xavier	Formalizing the Face Lattice of Polyhedra
B
Baader, Franz	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols Description Logics with Concrete Domains and General Concept Inclusions Revisited
Baanen, Anne	A Lean tactic for normalising ring expressions with exponents (short paper)
Baranowski, Marek	An SMT Theory of Fixed-Point Arithmetic
Barbosa, Haniel	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
Barnett, Lee A.	Covered Clauses Are Not Propagation Redundant
Barrett, Clark	Politeness for The Theory of Algebraic Datatypes Domain-Specific Reasoning with Satisfiability Modulo Theories A Decision Procedure for String to Code Point Conversion
Basin, David	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Baumgartner, Peter	Possible Models Computation and Revision - A Practical Approach
Bhayat, Ahmed	A Knuth-Bendix-Like Ordering for Orienting Combinator Equations A Combinator-Based Superposition Calculus for Higher-Order Logic A Polymorphic Vampire (short paper)
Biere, Armin	Covered Clauses Are Not Propagation Redundant
Blackburn, Patrick	Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
Blanchette, Jasmin	A Comprehensive Framework for Saturation Theorem Proving
Blazy, Sandrine	A Fast Verified Liveness Analysis in SSA form
Bohrer, Brandon	Constructive Hybrid Games
Bonacina, Maria Paola	SGGS Decision Procedures
Brakensiek, Joshua	The Resolution of Keller's Conjecture
Bray, Matthew	The Imandra Automated Reasoning System (system description)
Bride, Hadrien	N-PAT: A Nested Model-Checker (system description)
C
Cai, Cheng-Hao	N-PAT: A Nested Model-Checker (system description)
Calvanese, Diego	Combined Covers and Beth Definability
Cerna, David	Covered Clauses Are Not Propagation Redundant
Chew, Leroy	How QBF Expansion Makes Strategy Extraction Hard
Chlipala, Adam	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Chvalovský, Karel	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Clymo, Judith	How QBF Expansion Makes Strategy Extraction Hard
Cohen, Cyril	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
Cohen, Liron	Integrating Induction and Coinduction via Closure Operators and Proof Cycles
Cruanes, Simon	The Imandra Automated Reasoning System (system description)
Czajka, Lukasz	Practical proof search for Coq by type inhabitation
D
Dalmonte, Tiziano	HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description)
Dardinier, Thibault	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
De Angelis, Emanuele	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
de Moura, Leonardo	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
de Vilhena, Paulo Emílio	Algebraically Closed Fields in Isabelle/HOL
Delaware, Benjamin	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Dong, Jin Song	N-PAT: A Nested Model-Checker (system description)
Duarte, André	Implementing superposition in iProver (system description)
Dutertre, Bruno	Solving bit-vectors with MCSAT: explanations from bits and pieces
E
Eßmann, Robin	Verified Approximation Algorithms
F
Fioravanti, Fabio	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
Fontaine, Pascal	Politeness for The Theory of Algebraic Datatypes
From, Asta Halkjær	Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
Fürer, Basil	Quotients of Bounded Natural Functors
G
Ghilardi, Silvio	Combined Covers and Beth Definability
Gianola, Alessandro	Combined Covers and Beth Definability
Giesl, Jürgen	Termination Competition
Girlando, Marianna	Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description)
Gleiss, Bernhard	Subsumption Demodulation in First-Order Theorem Proving Layered Clause Selection for Theory Reasoning (short paper)
Gligoric, Milos	Deep Generation of Coq Lemma Names Using Elaborated Terms
Goertzel, Zarathustra	Make E Smart Again (short paper)
Gore, Rajeev	N-PAT: A Nested Model-Checker (system description)
Graham-Lengrand, Stéphane	Solving bit-vectors with MCSAT: explanations from bits and pieces
Gross, Jason	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Gunther, Emmanuel	Formalization of Forcing in Isabelle/ZF
Gutiérrez, Raúl	mu-term: Verify Termination Properties Automatically (system description) Automatically Proving and Disproving Feasibility Conditions
Guttmann, Walter	Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL
H
Hague, Matthew	Monadic Decomposition in Integer Linear Arithmetic
Hales, Thomas	Formal Proof of the Group Law for Edwards Elliptic Curves
Harrison, John	Adventures in Verifying Arithmetic
Hashim, Mohammed	Sequoia: a playground for logicians (system description)
Hausmann, Daniel	NP Reasoning in the Monotone mu-Calculus
He, Shaobo	An SMT Theory of Fixed-Point Arithmetic
Heimes, Lukas	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Heule, Marijn	The Resolution of Keller's Conjecture
Hou, Zhe	N-PAT: A Nested Model-Checker (system description)
I
Ignatovich, Denis	The Imandra Automated Reasoning System (system description)
J
Jakubuv, Jan	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Jovanović, Dejan	Solving bit-vectors with MCSAT: explanations from bits and pieces
K
Kagan, Elijah	The Imandra Automated Reasoning System (system description)
Kanishev, Konstantin	The Imandra Automated Reasoning System (system description)
Kanovich, Max	Soft subexponentials and multiplexing
Kapur, Deepak	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
Katz, Ricardo David	Formalizing the Face Lattice of Polyhedra
Kerjean, Marie	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
Kirst, Dominik	Trakhtenbrot's Theorem in Coq
Kohlhase, Michael	Logic-Independent Proof Search in Logical Frameworks (short paper)
Korovin, Konstantin	Implementing superposition in iProver (system description)
Kovacs, Laura	Subsumption Demodulation in First-Order Theorem Proving
Krstic, Srdjan	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Kuznetsov, Stepan	Soft subexponentials and multiplexing
L
Lammich, Peter	Efficient Verified Implementation of Introsort and Pdqsort
Lampert, Timm	Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates
Lange, Jane	Politeness for The Theory of Algebraic Datatypes
Larchey-Wendling, Dominique	Trakhtenbrot's Theorem in Coq
Larraz, Daniel	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
Lechner, Mathias	An SMT Theory of Fixed-Point Arithmetic
Li, Junyi Jessy	Deep Generation of Coq Lemma Names Using Elaborated Terms
Lin, Anthony Widjaja	Monadic Decomposition in Integer Linear Arithmetic
Lochbihler, Andreas	Quotients of Bounded Natural Functors
Lucas, Salvador	mu-term: Verify Termination Properties Automatically (system description) Automatically Proving and Disproving Feasibility Conditions
Léchenet, Jean-Christophe	A Fast Verified Liveness Analysis in SSA form
M
Mackey, John	The Resolution of Keller's Conjecture
Maclean, Ewen	The Imandra Automated Reasoning System (system description)
Mahboubi, Assia	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
Mahony, Brendan	N-PAT: A Nested Model-Checker (system description)
Maric, Filip	Verifying Faradžev-Read type Isomorph-Free Exhaustive Generation
Marin, Sonia	Focusing, axioms and synthetic inference rules (extended abstract)
McCarthy, Jim	N-PAT: A Nested Model-Checker (system description)
Miller, Dale	Focusing, axioms and synthetic inference rules (extended abstract)
Mometto, Nicola	The Imandra Automated Reasoning System (system description)
Montali, Marco	Combined Covers and Beth Definability
N
Naeem, Zan	Sequoia: a playground for logicians (system description)
Nakano, Anderson	Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates
Narvaez, David	The Resolution of Keller's Conjecture
Nguyen, Thanh Son	An SMT Theory of Fixed-Point Arithmetic
Nie, Pengyu	Deep Generation of Coq Lemma Names Using Elaborated Terms
Nigam, Vivek	Soft subexponentials and multiplexing
Nipkow, Tobias	Verified Approximation Algorithms Verification of Closest Pair of Points Algorithms
Noetzli, Andres	A Decision Procedure for String to Code Point Conversion
Norrish, Michael	Mechanised Modal Model Theory
O
Olivetti, Nicola	HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description)
Olšák, Miroslav	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
P
Pagano, Miguel	Formalization of Forcing in Isabelle/ZF
Palmskog, Karl	Deep Generation of Coq Lemma Names Using Elaborated Terms
Passmore, Grant	The Imandra Automated Reasoning System (system description)
Paulson, Lawrence	Algebraically Closed Fields in Isabelle/HOL
Pease, Adam	A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description) Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)
Pettorossi, Alberto	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
Pichardie, David	A Fast Verified Liveness Analysis in SSA form
Pimentel, Elaine	Focusing, axioms and synthetic inference rules (extended abstract)
Piotrowski, Bartosz	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Piskac, Ruzica	Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints
Pit-Claudel, Clément	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Platzer, André	Constructive Hybrid Games
Pozzato, Gian Luca	HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description)
Proietti, Maurizio	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
R
Rabe, Florian	Logic-Independent Proof Search in Logical Frameworks (short paper)
Rakamaric, Zvonimir	An SMT Theory of Fixed-Point Arithmetic
Raszyk, Martin	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Rath, Jakob	Subsumption Demodulation in First-Order Theorem Proving
Rau, Martin	Verification of Closest Pair of Points Algorithms
Raya, Rodrigo	Formal Proof of the Group Law for Edwards Elliptic Curves
Reger, Giles	A Knuth-Bendix-Like Ordering for Orienting Combinator Equations A Combinator-Based Superposition Calculus for Higher-Order Logic A Polymorphic Vampire (short paper)
Reis, Giselle	Sequoia: a playground for logicians (system description)
Reynolds, Andrew	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis A Decision Procedure for String to Code Point Conversion
Ringeissen, Christophe	Politeness for The Theory of Algebraic Datatypes
Rivkin, Andrey	Combined Covers and Beth Definability
Robillard, Simon	A Comprehensive Framework for Saturation Theorem Proving Verified Approximation Algorithms
Rouhling, Damien	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
Rowe, Reuben	Integrating Induction and Coinduction via Closure Operators and Proof Cycles
Ruemmer, Philipp	Monadic Decomposition in Integer Linear Arithmetic
Rydval, Jakub	Description Logics with Concrete Domains and General Concept Inclusions Revisited
S
Sacerdoti Coen, Claudio	Logic-Independent Proof Search in Logical Frameworks (short paper)
Sakaguchi, Kazuhiko	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis Validating Mathematical Structures
Scedrov, Andre	Soft subexponentials and multiplexing
Schaefer, Jan Frederik	Logic-Independent Proof Search in Logical Frameworks (short paper)
Schneider, Joshua	Quotients of Bounded Natural Functors A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Schröder, Lutz	NP Reasoning in the Monotone mu-Calculus
Schulz, Stephan	Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)
Sheng, Ying	Politeness for The Theory of Algebraic Datatypes
Straßburger, Lutz	Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description)
Strub, Pierre-Yves	Formalizing the Face Lattice of Polyhedra
Suda, Martin	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) Layered Clause Selection for Theory Reasoning (short paper)
Sutcliffe, Geoff	The CADE ATP System Competition Presentation
Sánchez Terraf, Pedro	Formalization of Forcing in Isabelle/ZF
T
Tinelli, Cesare	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis A Decision Procedure for String to Code Point Conversion
Tourret, Sophie	A Comprehensive Framework for Saturation Theorem Proving
Traytel, Dmitriy	Quotients of Bounded Natural Functors A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
U
Ullrich, Sebastian	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Urban, Josef	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) Prolog Technology Reinforcement Learning Prover (system description)
V
Villadsen, Jørgen	Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
Volpe, Marco	Focusing, axioms and synthetic inference rules (extended abstract)
W
Waldmann, Uwe	A Comprehensive Framework for Saturation Theorem Proving
Wang, Peng	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Winkler, Sarah	SGGS Decision Procedures
Wu, Zhilin	Monadic Decomposition in Integer Linear Arithmetic
X
Xu, Yiming	Mechanised Modal Model Theory
Z
Zohar, Yoni	Politeness for The Theory of Algebraic Datatypes
Zombori, Zsolt	Prolog Technology Reinforcement Learning Prover (system description)

Disclaimer | Powered by EasyChair Smart Program