Finding connections via satisfiability solving
From MaRDI portal
Cites work
- An abstract decision procedure for a theory of inductive data types.
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- AVATAR: The Architecture for First-Order Theorem Provers
- Cadiback: Extracting backbones with CaDiCaL
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Computing small unsatisfiable cores in satisfiability modulo theories
- Connection methods in linear logic and proof nets construction
- Constraint learning for non-confluent proof search
- Counterexample-guided abstraction refinement for symbolic model checking
- Efficient CNF encoding of Boolean cardinality constraints
- Efficient E-Matching for SMT Solvers
- Eliminating models during model elimination
- Encoding First Order Proofs in SAT
- Encoding first order proofs in SMT
- Faster, higher, stronger: E 2.3
- Handbook of satisfiability. In 2 parts
- scientific article; zbMATH DE number 1748580 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- scientific article; zbMATH DE number 1931669 (Why is no real title available?)
- scientific article; zbMATH DE number 1418280 (Why is no real title available?)
- scientific article; zbMATH DE number 1414298 (Why is no real title available?)
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Internal guidance for Satallax
- IPASIR-up: user propagators for CDCL
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Matings in matrices
- Model elimination and connection tableau procedures
- Normal form transformations
- On connections and higher-order logic
- Paramodulation-based theorem proving
- Proving Theorems with the Modification Method
- SAT-Based Subsumption Resolution
- SETHEO: A high-performance theorem prover
- Symmetry avoidance in MACE-style finite model finding
- Term indexing
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
This page was built for publication: Finding connections via satisfiability solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860393)
