iProver

swMATH9707MaRDI QIDQ21686FDOQ21686

Author name not available (Why is that?)

Cited In (64)

• Complexity of translations from resolution to sequent calculus
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Title not available (Why is that?)
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• 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
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• 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
• The Relative Power of Semantics and Unification
• Extensional higher-order paramodulation in Leo-III
• 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
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• 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
• Reducing higher-order theorem proving to a sequence of SAT problems
• SMELS: satisfiability modulo equality with lazy superposition
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Title not available (Why is that?)
• 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
• Solving dependency quantified Boolean formulas using quantifier localization
• Efficient CNF simplification based on binary implication graphs
• 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
• 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
• Implementing Superposition in iProver (System Description)
• Satisfiability modulo theories
• Efficient Low-Level Connection Tableaux
• An abstraction-refinement framework for reasoning with large theories
• Non-cyclic sorts for first-order satisfiability
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• A comprehensive framework for saturation theorem proving
• Experimenting with deduction modulo
• Ground joinability and connectedness in the superposition calculus
• One logic to use them all
• History and prospects for first-order automated deduction
• Detection of First Order Axiomatic Theories
• 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)
• SGGS decision procedures

This page was built for software: iProver