swMATH9707MaRDI QIDQ21686FDOQ21686
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007%2F978-3-540-71070-7_24
Cited In (only showing first 100 items - show all)
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Scavenger 0.1: a theorem prover based on conflict resolution
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- The Relative Power of Semantics and Unification
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Adding decision procedures to SMT solvers using axioms with triggers
- Semantically-guided goal-sensitive reasoning: model representation
- Exploring theories with a model-finding assistant
- Extensional crisis and proving identity
- A combined superposition and model evolution calculus
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Reducing higher-order theorem proving to a sequence of SAT problems
- Efficient CNF simplification based on binary implication graphs
- Invariant and type inference for matrices
- Aligator
- OTTER
- VAMPIRE
- Darwin
- SPASS
- TPTP
- SPASS+T
- Prover9
- DCTP
- SATCHMO
- E-Darvin
- AURA
- Zenon
- CERES
- StarExec
- iProver-Eq
- HeerHugo
- Equinox
- JAMPACK
- TLAPS
- E Theorem Prover
- FoCaLiZe
- Easychair
- Beagle
- dedukti
- Lingva
- E-MaLeS
- EQP
- Combining instance generation and resolution
- BliStrTune
- CoqMT
- CLIN
- DISCOUNT
- SNARK
- Waldmeister
- E-KRHyper
- UCPOP
- SRASS
- InKreSAT
- Peers-mcd
- Scavenger
- AVATAR
- HQSpre
- MadMax
- Focalide
- Superposition Calculus
- Twee
- BDDTab
- GKC
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Quantifier instantiation techniques for finite model finding in SMT
- Model evolution with equality -- revised and implemented
- Satisfiability modulo theories
- Efficient Low-Level Connection Tableaux
- ast2vec
- Ordered_Resolution_Prover
- Saturation_Framework
- Razor
- SPASS-AR
- PyRes
- Non-cyclic sorts for first-order satisfiability
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Experimenting with deduction modulo
- Ground joinability and connectedness in the superposition calculus
- lazyCoP
- One logic to use them all
- Q3B
- Complexity of fixed-size bit-vector logics
- Theorem proving as constraint solving with coherent logic
- The Matita interactive theorem prover
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Koala
- Lash
- Old or heavy? Decaying gracefully with age/weight shapes
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- SCL(EQ): SCL for first-order logic with equality
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
This page was built for software: iProver
