StarExec

swMATH8839MaRDI QIDQ20838FDOQ20838

Author name not available (Why is that?)

Cited In (62)

• The CADE-26 automated theorem proving system competition -- CASC-26
• Making higher-order superposition work
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• SAT-Inspired Eliminations for Superposition
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• The 10th IJCAR automated theorem proving system competition -- CASC-J10
• Old or heavy? Decaying gracefully with age/weight shapes
• Restricted combinatory unification
• Faster, higher, stronger: E 2.3
• Multi-dimensional interpretations for termination of term rewriting
• Scavenger 0.1: a theorem prover based on conflict resolution
• Title not available (Why is that?)
• Term orderings for non-reachability of (conditional) rewriting
• Synthesis of domain specific CNF encoders for bit-vector solvers
• The \textsc{SDEval} benchmarking toolkit
• Title not available (Why is that?)
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• On solving quantified bit-vector constraints using invertibility conditions
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Learning Optimal Decision Sets and Lists with SAT
• The 2013 evaluation of SMT-COMP and SMT-LIB
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• Performance of clause selection heuristics for saturation-based theorem proving
• Incomplete SMT techniques for solving non-linear formulas over the integers
• Proving termination through conditional termination
• Scaling enumerative program synthesis via divide and conquer
• A calculus for modular loop acceleration
• Making higher-order superposition work
• A combinator-based superposition calculus for higher-order logic
• Layered clause selection for theory reasoning (short paper)
• Selecting the selection
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• Title not available (Why is that?)
• Refutation-based synthesis in SMT
• Title not available (Why is that?)
• Machine learning-based restart policy for CDCL SAT solvers
• Subsumption demodulation in first-order theorem proving
• Finding Finite Models in Multi-sorted First-Order Logic
• Deciding local theory extensions via E-matching
• SAT race 2015
• The CADE-27 automated theorem proving system competition -- CASC-27
• Superposition with first-class booleans and inprocessing clausification
• A FOOLish encoding of the next state relations of imperative programs
• Datatypes with shared selectors
• Superposition for \(\lambda\)-free higher-order logic
• Induction with generalization in superposition reasoning
• Confluence Competition 2015
• Induction in saturation-based proof search
• An empirical study of branching heuristics through the lens of global learning rate
• Incremental bounded model checking for embedded software
• A decision procedure for (co)datatypes in SMT solvers
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• A decision procedure for (co)datatypes in SMT solvers
• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Splitting proofs for interpolation
• Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19--22, 2014. Proceedings
• Symmetry avoidance in MACE-style finite model finding
• A Polymorphic Vampire
• \textsf{Open-WBO-Inc}: approximation strategies for incomplete weighted MaxSAT
• Learning rate based branching heuristic for SAT solvers
• An efficient SMT solver for string constraints
• SAT competition 2020

This page was built for software: StarExec