scientific article; zbMATH DE number 837700
From MaRDI portal
Publication:4863622
zbMATH Open0848.68101MaRDI QIDQ4863622FDOQ4863622
Authors: Melvin Fitting 
Publication date: 24 January 1996
Title of this publication is not available (Why is that?)
Recommendations
- scientific article; zbMATH DE number 193652
- Logic for informatics and artificial intelligence
- scientific article; zbMATH DE number 4155933
- Logic and reasoning
- Publication:4729755
- scientific article; zbMATH DE number 46359
- scientific article; zbMATH DE number 53085
- scientific article; zbMATH DE number 3976991
- Logic. The short method
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)
Cited In (only showing first 100 items - show all)
- Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography
- Minimal model generation with positive unit hyper-resolution tableaux
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- A Unifying Perspective on Knowledge Updates
- On partial and paraconsistent logics
- Interpolation for first order S5
- Theorem proving with bounded rigid \(E\)-unification
- First order Stålmarck. Universal lemmas through branch merges
- Title not available (Why is that?)
- Linearity and regularity with negation normal form
- Differential dynamic logic for hybrid systems
- Trace-length independent runtime monitoring of quantitative policies in LTL
- A sound and complete model-generation procedure for consistent and confidentiality-preserving databases
- Binary resolution over Boolean lattices
- On multiple conclusion deductions in classical logic
- \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
- First-order theorem proving: foreword
- Incremental variable splitting
- Title not available (Why is that?)
- Formalization of the resolution calculus for first-order logic
- Ordered tableaux: extensions and applications
- Interpolation systems for ground proofs in automated deduction: a survey
- Title not available (Why is that?)
- An intensional type theory: Motivation and cut-elimination
- Higher-order semantics and extensionality
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Automated proof-searching for strong Kleene logic and its binary extensions via correspondence analysis
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Title not available (Why is that?)
- A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
- Liberalized variable splitting
- Hilbert's epsilon as an operator of indefinite committed choice
- The lazy logic of partial terms
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Tractable query answering and rewriting under description logic constraints
- Passive induction and a solution to a Paris-Wilkie open question
- Superposition-based equality handling for analytic tableaux
- The disconnection tableau calculus
- Correspondence analysis and automated proof-searching for first degree entailment
- Combining answer set programming with description logics for the semantic web
- Depth-first proof search without backtracking for free-variable clausal tableaux
- Free variable tableaux for propositional modal logics
- Soundness and completeness proofs by coinductive methods
- Reasoning about norms under uncertainty in dynamic environments
- Resolution is cut-free
- Formalization of reliability block diagrams in higher-order logic
- Local closed world reasoning with description logics under the well-founded semantics
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- KeY: A Formal Method for Object-Oriented Systems
- Simulating Dynamic Systems Using Linear Time Calculus Theories
- Decision procedures for region logic
- Resolution based algorithms for the transversal hypergraph generation problem
- Many-Valued Non-deterministic Semantics for First-Order Logics of Formal (In)consistency
- Understanding the Brandenburger-Keisler paradox
- FLP answer set semantics without circular justifications for general logic programs
- Reasoning in description logics by a reduction to disjunctive datalog
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation
- Hall's theorem for enumerable families of finite sets
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi
- Regaining cut admissibility in deduction modulo using abstract completion
- Integration of a security type system into a program logic
- Intensional models for the theory of types
- Formal verification of a generic framework to synthesize SAT-provers
- Towards the formal reliability analysis of oil and gas pipelines
- Extended First-Order Logic
- Connection calculus theorem proving with multiple built-in theories
- Efficient algorithms for bounded rigid \(E\)-unification
- A tableau-based decision procedure for a fragment of set theory with iterated membership
- Automatic models of first order theories
- Tableau systems for deontic action logics based on finite Boolean algebras, and their complexity
- Blocking and other enhancements for bottom-up model generation methods
- Free-variable semantic tableaux for the logic of fuzzy inequalities
- Synthetic tableaux: Minimal tableau search heuristics
- Deduction by combining semantic tableaux and integer programming
- Reasoning with preorders and dynamic sorts using free variable tableaux
- Lean induction principles for tableaux
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
- A framework for using knowledge in tableau proofs
- Tableaux and interpolation for propositional justification logics
- A semantics for nabla
- Local confluence of conditional and generalized term rewriting systems
- An abductive Question-Answer System for the minimal logic of formal inconsistency \(\mathsf{mbC}\)
- Reasoning in the theory of heap: satisfiability and interpolation
- Reasoning with uncertain and inconsistent OWL ontologies
- Title not available (Why is that?)
- The tableau-based theorem prover 3 T A P Version 4.0
- Free variables and theories: revisiting rigid \(E\)-unification
- Reasoning on with Defeasibility in ASP
- Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
- Dual tableau-based decision procedures for fragments of the logic of binary relations
- Interactive matching logic proofs in Coq
- On enumerating query plans using analytic tableau
- Cut and gamma. I: Propositional and constant domain \textbf{R}
- A proof-planning framework with explicit abstractions based on indexed formulas
- Proving confluence in the confluence framework with confident
- Stoic Sequent Logic and Proof Theory
- Craig interpolation with clausal first-order tableaux
- Title not available (Why is that?)
- Tableau methods for a logic with term declarations
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4863622)
