Pages that link to "Item:Q2724150"
From MaRDI portal
The following pages link to Handbook of automated reasoning. In 2 vols (Q2724150):
Displaying 50 items.
- Inference engine based on closure and join operators over truth table binary relations (Q406448) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Efficient general AGH-unification (Q462489) (← links)
- Glushkov's evidence algorithm (Q466397) (← links)
- Enhancing unsatisfiable cores for LTL with information on temporal relevance (Q507378) (← links)
- Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) (Q631075) (← links)
- Models and the dynamics of theory-building in physics. I: Modeling strategies (Q643103) (← links)
- The Logics' Explorer: a Maple package for exploring finite many-valued propositional logics (Q692319) (← links)
- Clausal presentation of theories in deduction modulo (Q744331) (← links)
- Formal analysis of symbolic authenticity (Q831950) (← links)
- The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem (Q843609) (← links)
- Optimal length resolution refutations of difference constraint systems (Q846163) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Normal forms for fuzzy logics: a proof-theoretic approach (Q884948) (← links)
- Proof systems for planning under 0-approximation semantics (Q893736) (← links)
- On the counting complexity of propositional circumscription (Q963360) (← links)
- Resolution is cut-free (Q972424) (← links)
- Tractable query answering and rewriting under description logic constraints (Q975872) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Computing finite models by reduction to function-free clause logic (Q1006733) (← links)
- First order Stålmarck. Universal lemmas through branch merges (Q1040785) (← links)
- Orienting rewrite rules with the Knuth-Bendix order. (Q1401932) (← links)
- Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques (Q1581359) (← links)
- Automating formalization by statistical and semantic parsing of mathematics (Q1687711) (← links)
- An overview of automated reasoning and related fields (Q1819948) (← links)
- Reasoning processes in propositional logic (Q1959223) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Normal forms of conditional knowledge bases respecting system P-entailments and signature renamings (Q2075376) (← links)
- Solving bitvectors with MCSAT: explanations from bits and pieces (Q2096440) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Semantic relevance (Q2104509) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- Contradiction separation based dynamic multi-clause synergized automated deduction (Q2198231) (← links)
- Copy complexity of Horn formulas with respect to unit read-once resolution (Q2235734) (← links)
- Semantic classification of qualitative conditionals and calculating closures of nonmonotonic inference relations (Q2237135) (← links)
- Reasoning about truth in first-order logic (Q2255212) (← links)
- Alternating two-way AC-tree automata (Q2373699) (← links)
- Proof planning with multiple strategies (Q2389631) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols (Q2424886) (← links)
- Resolution with order and selection for hybrid logics (Q2429982) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Reasoning on UML class diagrams (Q2457652) (← links)
- On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743) (← links)
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically (Q2484410) (← links)
- Efficient instance retrieval with standard and relational path indexing (Q2486586) (← links)
- Referential logic of proofs (Q2500486) (← links)
- Sequent forms of Herbrand theorem and their applications (Q2502163) (← links)
- Shallow confluence of conditional term rewriting systems (Q2518609) (← links)
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) (Q2577589) (← links)
