iProver
From MaRDI portal
IProver
Cited in
(only showing first 100 items - show all)- Old or heavy? Decaying gracefully with age/weight shapes
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- 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
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- A neurally-guided, parallel theorem prover
- 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
- Certified DQBF solving by definition extraction
- DQBDD: an efficient BDD-based DQBF solver
- Extensional higher-order paramodulation in Leo-III
- The Relative Power of Semantics and Unification
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Adding decision procedures to SMT solvers using axioms with triggers
- Semantically-guided goal-sensitive reasoning: model representation
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- A combined superposition and model evolution calculus
- Exploring theories with a model-finding assistant
- Extensional crisis and proving identity
- SMELS: satisfiability modulo equality with lazy superposition
- Reducing higher-order theorem proving to a sequence of SAT problems
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Reducing higher-order theorem proving to a sequence of SAT problems
- Solving dependency quantified Boolean formulas using quantifier localization
- Efficient CNF simplification based on binary implication graphs
- 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
- BliStrTune
- CoqMT
- CLIN
- DISCOUNT
- SNARK
- Waldmeister
- E-KRHyper
- UCPOP
- SRASS
- InKreSAT
- Peers-mcd
- Scavenger
- AVATAR
- HQSpre
- MadMax
- Focalide
- Superposition Calculus
- Twee
- BDDTab
- GKC
- ast2vec
- Ordered_Resolution_Prover
- Saturation_Framework
- Razor
- SPASS-AR
- Complexity of translations from resolution to sequent calculus
- Invariant and type inference for matrices
- GRUNGE: a grand unified ATP challenge
- Finding Finite Models in Multi-sorted First-Order Logic
- Combining instance generation and resolution
- CTL model checking in deduction modulo
- Model evolution with equality -- revised and implemented
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Quantifier instantiation techniques for finite model finding in SMT
- Satisfiability modulo theories
- Implementing Superposition in iProver (System Description)
- An abstraction-refinement framework for reasoning with large theories
This page was built for software: iProver
