Cited in
(only showing first 100 items - show all)- 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
- Making higher-order superposition work
- A FOOLish encoding of the next state relations of imperative programs
- Datatypes with shared selectors
- Superposition for -free higher-order logic
- Lash
- Confluence Competition 2015
- An empirical study of branching heuristics through the lens of global learning rate
- Incremental bounded model checking for embedded software
- Induction in saturation-based proof search
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- A decision procedure for (co)datatypes in SMT solvers
- A decision procedure for (co)datatypes in SMT solvers
- PyRes
- PReLearn
- iRankFinder
- Open-WBO-Inc
- cake_lpr
- SLIME
- 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 9th IJCAR automated theorem proving system competition -- CASC-J9
- NaTT
- Symmetry avoidance in MACE-style finite model finding
- SAT-Inspired Eliminations for Superposition
- 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
- Leviathan
- qbf2epr
- SaDiCaL
- SAT competition 2020
- TreeAutomizer
- Aalta
- Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
- Old or heavy? Decaying gracefully with age/weight shapes
- Restricted combinatory unification
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Faster, higher, stronger: E 2.3
- Multi-dimensional interpretations for termination of term rewriting
- The CADE-26 automated theorem proving system competition -- CASC-26
- Scavenger 0.1: a theorem prover based on conflict resolution
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- Term orderings for non-reachability of (conditional) rewriting
- Synthesis of domain specific CNF encoders for bit-vector solvers
- The \textsc{SDEval} benchmarking toolkit
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- On solving quantified bit-vector constraints using invertibility conditions
- Counterexample-guided quantifier instantiation for synthesis in SMT
- The 2013 evaluation of SMT-COMP and SMT-LIB
- Learning Optimal Decision Sets and Lists with SAT
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- Performance of clause selection heuristics for saturation-based theorem proving
- Proving termination through conditional termination
- Scaling enumerative program synthesis via divide and conquer
- Incomplete SMT techniques for solving non-linear formulas over the integers
- A calculus for modular loop acceleration
- A combinator-based superposition calculus for higher-order logic
- Layered clause selection for theory reasoning (short paper)
- Selecting the selection
- Making higher-order superposition work
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- scientific article; zbMATH DE number 7359428 (Why is no real title available?)
- Refutation-based synthesis in SMT
- scientific article; zbMATH DE number 7471678 (Why is no real title available?)
- Machine learning-based restart policy for CDCL SAT solvers
- HaifaSat
- FLATA
- SMT-LIB
- TPTP
- SPASS+T
- PURRS
- PoCaB
- Satallax
- NiVER
- Zeno
- Asparagus
- RunLim
- Runsolver
- CVC4
- Bloqqer
- Aligators
- Eldarica
- CoLoR
- MU-TERM
- TPDB
- GQML
- MetTeL
- Kaluza
- Easychair
- Beagle
- Ctrl
This page was built for software: StarExec
