Abstract is missing.
- A Logical Framework for Developing and Mechanizing Set TheoriesArnon Avron. 3-8 [doi]
- Programming by Examples: Applications, Algorithms, and Ambiguity ResolutionSumit Gulwani. 9-14 [doi]
- Logic & Proofs for Cyber-Physical SystemsAndré Platzer. 15-21 [doi]
- A Verified SAT Solver Framework with Learn, Forget, Restart, and IncrementalityJasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach. 25-44 [doi]
- Super-Blocked ClausesBenjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere. 45-61 [doi]
- Counting Constraints in Flat Array FragmentsFrancesco Alberti, Silvio Ghilardi, Elena Pagani. 65-81 [doi]
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMTKshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli. 82-98 [doi]
- Congruence Closure in Intensional Type TheoryDaniel Selsam, Leonardo de Moura. 99-115 [doi]
- Fast Cube Tests for LIA Constraint SolvingMartin Bromberger, Christoph Weidenbach. 116-132 [doi]
- Model Finding for Recursive Functions in SMTAndrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli. 133-151 [doi]
- Colors Make Theories HardRoberto Sebastiani. 152-170 [doi]
- Nominal Confluence ToolTakahito Aoto 0001, Kentaro Kikuchi. 173-182 [doi]
- Built-in Variant Generation and Unification, and Their Applications in Maude 2.7Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Carolyn L. Talcott. 183-192 [doi]
- Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUFTing Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen. 195-212 [doi]
- Race Against the Teens - Benchmarking Mechanized Math on Pre-university ProblemsTakuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai, Noriko H. Arai. 213-227 [doi]
- raSAT: An SMT Solver for Polynomial ConstraintsVu Xuan Tung, To Van Khanh, Mizuhito Ogawa. 228-237 [doi]
- Schematic Cut Elimination and the Ordered Pigeonhole PrincipleDavid M. Cerna, Alexander Leitsch. 241-256 [doi]
- Subsumption Algorithms for Three-Valued Geometric ResolutionHans de Nivelle. 257-272 [doi]
- On Interpolation and Symbol Elimination in Theory ExtensionsViorica Sofronie-Stokkermans. 273-289 [doi]
- System Description: GAPT 2.0Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner, Sebastian Zivota. 293-301 [doi]
- nanoCoP: A Non-clausal Connection ProverJens Otten. 302-312 [doi]
- Selecting the SelectionKrystof Hoder, Giles Reger, Martin Suda 0001, Andrei Voronkov. 313-329 [doi]
- Performance of Clause Selection Heuristics for Saturation-Based Theorem ProvingStephan Schulz, Martin Möhrmann. 330-345 [doi]
- Internal Guidance for SatallaxMichael Färber, Chad Brown. 349-361 [doi]
- Effective Normalization Techniques for HOLMax Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller. 362-370 [doi]
- Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel CompositionJoseph Boudou. 373-388 [doi]
- Interval Temporal Logic Model Checking: The Border Between Good and Bad HS FragmentsLaura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala. 389-405 [doi]
- : A Resolution-Based Prover for Multimodal KCláudia Nalon, Ullrich Hustadt, Clare Dixon. 406-415 [doi]
- Inducing Syntactic Cut-Elimination for Indexed Nested SequentsRevantha Ramanayake. 416-432 [doi]
- A Tableau System for Quasi-Hybrid LogicDiana Costa, Manuel A. Martins. 435-451 [doi]
- Machine-Checked Interpolation Theorems for Substructural Logics Using Display CalculiJeremy E. Dawson, James Brotherston, Rajeev Goré. 452-468 [doi]
- Intuitionistic Layered Graph LogicSimon Docherty, David J. Pym. 469-486 [doi]
- Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent CalculiYoni Zohar, Anna Zamansky. 487-495 [doi]
- Model Checking Parameterised Multi-token Systems via the Composition MethodBenjamin Aminof, Sasha Rubin. 499-515 [doi]
- Unbounded-Thread Program Verification using Thread-State EquationsKonstantinos Athanasiou, Peizun Liu, Thomas Wahl. 516-531 [doi]
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data ConstraintsXincai Gu, Taolue Chen, Zhilin Wu. 532-549 [doi]
- Lower Runtime Bounds for Integer ProgramsFlorian Frohn, M. Naaf, Jera Hensel, Marc Brockschmidt, Jürgen Giesl. 550-567 [doi]
- Translating Scala Programs to Isabelle/HOL - System DescriptionLars Hupel, Viktor Kuncak. 568-577 [doi]