Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
From MaRDI portal
Publication:4916080
DOI10.1007/978-3-642-37651-1_10zbMath1385.68038OpenAlexW158985585MaRDI QIDQ4916080
Publication date: 19 April 2013
Published in: Programming Logics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_10
Related Items (19)
Semantically-guided goal-sensitive reasoning: model representation ⋮ Implementing Superposition in iProver (System Description) ⋮ Eliminating models during model elimination ⋮ Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ SCL clause learning from simple models ⋮ Faster, higher, stronger: E 2.3 ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ SGGS decision procedures ⋮ SCL(EQ): SCL for first-order logic with equality
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Eliminating dublication with the hyper-linking strategy
- Computing finite models by reduction to function-free clause logic
- Explicit representation of terms defined by counter examples
- A method for simultaneous search for refutations and models by equational constraint solving
- Ordered semantic hyper-linking
- Partial instantiation methods for inference in first-order logic
- Explicit versus implicit representations of subsets of the Herbrand universe.
- Sufficient-completeness, ground-reducibility and their complexity
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Extending a Resolution Prover for Inequalities on Elementary Functions
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Proof Systems for Effectively Propositional Logic
- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Combining Instance Generation and Resolution
- Proving Theorems with the Modification Method
- Term Rewriting and All That
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Clause Elimination Procedures for CNF Formulas
- Labelled Unit Superposition Calculi for Instantiation-Based Reasoning
- Computer Science Logic
- Theory and Applications of Satisfiability Testing
- Theory Instantiation
- Logic Programming and Nonmonotonic Reasoning
- Theory and Applications of Satisfiability Testing
- Interpolation and Symbol Elimination in Vampire
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- On the Saturation of YAGO
- Automated Deduction – CADE-19
This page was built for publication: Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
