Cited in
(only showing first 100 items - show all)- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Experimenting with deduction modulo
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- A combined superposition and model evolution calculus
- Adding decision procedures to SMT solvers using axioms with triggers
- Efficient CNF simplification based on binary implication graphs
- Semantically-guided goal-sensitive reasoning: model representation
- Reducing higher-order theorem proving to a sequence of SAT problems
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Non-cyclic sorts for first-order satisfiability
- Quantifier instantiation techniques for finite model finding in SMT
- The Matita interactive theorem prover
- Theorem proving as constraint solving with coherent logic
- Model evolution with equality -- revised and implemented
- Combining instance generation and resolution
- Ground joinability and connectedness in the superposition calculus
- 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
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Efficient Low-Level Connection Tableaux
- ast2vec
- Ordered_Resolution_Prover
- Saturation_Framework
- Razor
- SPASS-AR
- PyRes
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
- One logic to use them all
- Invariant and type inference for matrices
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- lazyCoP
- Q3B
- Exploring theories with a model-finding assistant
- Extensional crisis and proving identity
- Complexity of fixed-size bit-vector logics
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Scavenger 0.1: a theorem prover based on conflict resolution
- Satisfiability modulo theories
- The Relative Power of Semantics and Unification
- SGGS decision procedures
- Koala
- Lash
- SMELS: satisfiability modulo equality with lazy superposition
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- AC simplifications and closure redundancies in the superposition calculus
- Finding Finite Models in Multi-sorted First-Order Logic
- dCAQE
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
This page was built for software: iProver
