The following pages link to (Q4863622):
Displaying 50 items.
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- Formalization of reliability block diagrams in higher-order logic (Q334147) (← links)
- Automatic models of first order theories (Q387121) (← links)
- First-order theorem proving: foreword (Q429582) (← links)
- Incremental variable splitting (Q429591) (← links)
- \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps (Q429596) (← links)
- An interpolating sequent calculus for quantifier-free Presburger arithmetic (Q438556) (← links)
- Reasoning about norms under uncertainty in dynamic environments (Q465604) (← links)
- Tableau systems for deontic action logics based on finite Boolean algebras, and their complexity (Q526730) (← links)
- A sound and complete model-generation procedure for consistent and confidentiality-preserving databases (Q549726) (← links)
- Local closed world reasoning with description logics under the well-founded semantics (Q646502) (← links)
- On partial and paraconsistent logics (Q701297) (← links)
- Linearity and regularity with negation normal form (Q703486) (← links)
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (Q782499) (← links)
- A tableau-based decision procedure for a fragment of set theory with iterated membership (Q812437) (← links)
- Binary resolution over Boolean lattices (Q853473) (← links)
- A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux (Q877883) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Liberalized variable splitting (Q877894) (← links)
- Passive induction and a solution to a Paris-Wilkie open question (Q882120) (← links)
- Integration of a security type system into a program logic (Q935469) (← links)
- Hilbert's epsilon as an operator of indefinite committed choice (Q946570) (← links)
- Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography (Q953531) (← links)
- Resolution is cut-free (Q972424) (← links)
- Tractable query answering and rewriting under description logic constraints (Q975872) (← links)
- Differential dynamic logic for hybrid systems (Q1040772) (← links)
- First order Stålmarck. Universal lemmas through branch merges (Q1040785) (← links)
- Depth-first proof search without backtracking for free-variable clausal tableaux (Q1404980) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Synthetic tableaux: Minimal tableau search heuristics (Q2104533) (← links)
- An abductive Question-Answer System for the minimal logic of formal inconsistency \(\mathsf{mbC}\) (Q2118976) (← links)
- Reasoning in the theory of heap: satisfiability and interpolation (Q2119112) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Regaining cut admissibility in deduction modulo using abstract completion (Q2266989) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Resolution based algorithms for the transversal hypergraph generation problem (Q2310740) (← links)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- Free-variable semantic tableaux for the logic of fuzzy inequalities (Q2364294) (← links)
- Combining answer set programming with description logics for the semantic web (Q2389666) (← links)
- Languages of logic and their applications (Q2425445) (← links)
- FLP answer set semantics without circular justifications for general logic programs (Q2453743) (← links)
- Reasoning in description logics by a reduction to disjunctive datalog (Q2462648) (← links)
- Understanding the Brandenburger-Keisler paradox (Q2464651) (← links)
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) (Q2577589) (← links)
- Formal verification of a generic framework to synthesize SAT-provers (Q2583288) (← links)
- Correspondence analysis and automated proof-searching for first degree entailment (Q2663794) (← links)
- Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
- A qualitative temporal extension of here-and-there logic (Q2694563) (← links)
