iProver
From MaRDI portal
IProver
Cited in
(only showing first 100 items - show all)- Efficient Low-Level Connection Tableaux
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Non-cyclic sorts for first-order satisfiability
- Koala
- Lash
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- A comprehensive framework for saturation theorem proving
- Experimenting with deduction modulo
- PyRes
- lazyCoP
- Q3B
- Ground joinability and connectedness in the superposition calculus
- One logic to use them all
- Complexity of fixed-size bit-vector logics
- History and prospects for first-order automated deduction
- Detection of First Order Axiomatic Theories
- Theorem proving as constraint solving with coherent logic
- The Matita interactive theorem prover
- dCAQE
- QESTO
- scientific article; zbMATH DE number 7178363 (Why is no real title available?)
- SGGS decision procedures
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- 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
This page was built for software: iProver
