scientific article; zbMATH DE number 837700

Publication date: 24 January 1996

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

first-order logic Hilbert systems proof procedures

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Related Items

Soundness and completeness proofs by coinductive methods, Free-variable semantic tableaux for the logic of fuzzy inequalities, Decision Procedures for Region Logic, Interpolation systems for ground proofs in automated deduction: a survey, Theorem Proving with Bounded Rigid E-Unification, Efficient Algorithms for Bounded Rigid E-unification, On Enumerating Query Plans Using Analytic Tableau, Extended First-Order Logic, Binary resolution over Boolean lattices, Exact Query Reformulation with First-Order Ontologies and Databases, A Unifying Perspective on Knowledge Updates, Formalization of reliability block diagrams in higher-order logic, Combining answer set programming with description logics for the semantic web, Higher-order semantics and extensionality, Infinite-Valued First-Order Łukasiewicz Logic: Hypersequent Calculi Without Structural Rules and Proof Search for Sentences in the Prenex Form, APPROXIMATING BEPPO LEVI’S PRINCIPIO DI APPROSSIMAZIONE, Formalization of the resolution calculus for first-order logic, Simulating Dynamic Systems Using Linear Time Calculus Theories, Correspondence analysis and automated proof-searching for first degree entailment, A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux, The disconnection tableau calculus, Superposition-based equality handling for analytic tableaux, Liberalized variable splitting, Craig interpolation with clausal first-order tableaux, Passive induction and a solution to a Paris-Wilkie open question, Unnamed Item, Reasoning on with Defeasibility in ASP, Languages of logic and their applications, Local confluence of conditional and generalized term rewriting systems, Hall's theorem for enumerable families of finite sets, Depth-first proof search without backtracking for free-variable clausal tableaux, Free Variables and Theories: Revisiting Rigid E-unification, Incremental variable splitting, \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps, A qualitative temporal extension of here-and-there logic, An interpolating sequent calculus for quantifier-free Presburger arithmetic, Lean induction principles for tableaux, Free variable tableaux for propositional modal logics, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, Ordered tableaux: Extensions and applications, A framework for using knowledge in tableau proofs, First-order automated reasoning with theories: when deduction modulo theory meets practice, Local closed world reasoning with description logics under the well-founded semantics, Reasoning about norms under uncertainty in dynamic environments, FLP answer set semantics without circular justifications for general logic programs, Integration of a security type system into a program logic, An intensional type theory: motivation and cut-elimination, Reasoning in description logics by a reduction to disjunctive datalog, Understanding the Brandenburger-Keisler paradox, Hilbert's epsilon as an operator of indefinite committed choice, Minimal model generation with positive unit hyper-resolution tableaux, The tableau-based theorem prover 3 T A P Version 4.0, Reasoning with Uncertain and Inconsistent OWL Ontologies, Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography, Tableau systems for deontic action logics based on finite Boolean algebras, and their complexity, Controlled use of clausal lemmas in connection tableau calculi, Tableau methods for a logic with term declarations, Connection calculus theorem proving with multiple built-in theories, On partial and paraconsistent logics, Resolution is cut-free, Many-Valued Non-deterministic Semantics for First-Order Logics of Formal (In)consistency, Linearity and regularity with negation normal form, A sound and complete model-generation procedure for consistent and confidentiality-preserving databases, KeY: A Formal Method for Object-Oriented Systems, Tractable query answering and rewriting under description logic constraints, Regaining cut admissibility in deduction modulo using abstract completion, An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic, Unnamed Item, Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL, Stoic Sequent Logic and Proof Theory, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis, Blocking and other enhancements for bottom-up model generation methods, CUT AND GAMMA I: PROPOSITIONAL AND CONSTANT DOMAIN R, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Resolution based algorithms for the transversal hypergraph generation problem, A semantics for nabla, A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas, Towards the Formal Reliability Analysis of Oil and Gas Pipelines, Differential dynamic logic for hybrid systems, First order Stålmarck. Universal lemmas through branch merges, Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation, α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic, Intensional models for the theory of types, Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\), Formal verification of a generic framework to synthesize SAT-provers, Synthetic tableaux: Minimal tableau search heuristics, A tableau-based decision procedure for a fragment of set theory with iterated membership, SAT-Inspired Eliminations for Superposition, Interpolation for first order S5, The lazy logic of partial terms, An abductive Question-Answer System for the minimal logic of formal inconsistency \(\mathsf{mbC}\), Reasoning in the theory of heap: satisfiability and interpolation