StarExec

swMATH8839MaRDI QIDQ20838FDOQ20838

Author name not available (Why is that?)

Cited In (62)

• Making higher-order superposition work
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• The CADE-26 automated theorem proving system competition – CASC-26
• SAT-Inspired Eliminations for Superposition
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• 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
• Learning Rate Based Branching Heuristic for SAT Solvers
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• Title not available (Why is that?)
• The CADE-27 Automated theorem proving System Competition – CASC-27
• 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
• Making higher-order superposition work
• A combinator-based superposition calculus for higher-order logic
• Layered clause selection for theory reasoning (short paper)
• The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• Title not available (Why is that?)
• Refutation-based synthesis in SMT
• Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
• Title not available (Why is that?)
• Machine learning-based restart policy for CDCL SAT solvers
• Open-WBO-Inc: Approximation Strategies for Incomplete Weighted MaxSAT
• Subsumption demodulation in first-order theorem proving
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• Finding Finite Models in Multi-sorted First-Order Logic
• Deciding local theory extensions via E-matching
• SAT race 2015
• Selecting the Selection
• The 10th IJCAR automated theorem proving system competition – CASC-J10
• Proving Termination Through Conditional Termination
• Scaling Enumerative Program Synthesis via Divide and Conquer
• 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
• 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
• The SDEval benchmarking toolkit
• Symmetry avoidance in MACE-style finite model finding
• Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
• A Polymorphic Vampire
• A Calculus for Modular Loop Acceleration
• An efficient SMT solver for string constraints
• A Decision Procedure for (Co)datatypes in SMT Solvers
• SAT competition 2020

This page was built for software: StarExec