The following pages link to (Q2751379):
Displaying 50 items.
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- On the verification of security-aware E-services (Q429592) (← links)
- Consequence-based and fixed-parameter tractable reasoning in description logics (Q490523) (← links)
- MPTP-motivation, implementation, first experiments (Q556682) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Simplifying proofs in Fitch-style natural deduction systems (Q851139) (← links)
- Attacking group protocols by refuting incorrect inductive conjectures (Q861695) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- Things to know when implementing KBO (Q861708) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Deciding expressive description logics in the framework of resolution (Q924723) (← links)
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Labelled splitting (Q1037396) (← links)
- Hyperresolution for guarded formulae (Q1404983) (← links)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)
- Superposition decides the first-order logic fragment over ground theories (Q1949088) (← links)
- Efficient local reductions to basic modal logic (Q2055845) (← links)
- A unifying splitting framework (Q2055869) (← links)
- Subsumption demodulation in first-order theorem proving (Q2096454) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Local is best: efficient reductions to modal logic \textsf{K} (Q2102930) (← links)
- SCL(EQ): SCL for first-order logic with equality (Q2104511) (← links)
- Local reductions for the modal cube (Q2104538) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Old or heavy? Decaying gracefully with age/weight shapes (Q2305433) (← links)
- Induction in saturation-based proof search (Q2305434) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Alternating two-way AC-tree automata (Q2373699) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically (Q2484410) (← links)
- Selecting the Selection (Q2817931) (← links)
- Unsorted Functional Translations (Q2825403) (← links)
- Presenting and Explaining Mizar (Q2867936) (← links)
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Q2964454) (← links)
- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation (Q2964455) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Automated Reasoning Building Blocks (Q3449631) (← links)
- Superposition for Fixed Domains (Q3540186) (← links)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance (Q3541722) (← links)
- Deciding the Inductive Validity of ∀ ∃ * Queries (Q3644758) (← links)
- Superposition Modulo Linear Arithmetic SUP(LA) (Q3655193) (← links)
- Simple and Efficient Clause Subsumption with Feature Vector Indexing (Q4913860) (← links)
