iProver

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