Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning

DOI10.1007/978-3-642-37651-1_10zbMath1385.68038OpenAlexW158985585MaRDI QIDQ4916080

Konstantin Korovin

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

• MiniSat
• OTTER
• VAMPIRE
• TPTP
• Darwin
• E-Darvin
• iProver-Eq
• iProver
• E Theorem Prover
• YAGO
• MSPASS
• DISCOUNT

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