scientific article

Publication date: 23 January 1993

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

completeness resolution soundness semantic tableaux

Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (88)

On the relative merits of path dissolution and the method of analytic tableaux ⋮ Accelerating tableaux proofs using compact representations ⋮ How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic q ⋮ A logic of separating modalities ⋮ Specification and Verification of Multi-Agent Systems ⋮ A tableau prover for domain minimization ⋮ The saturated tableaux for linear miniscope Horn-like temporal logic ⋮ The liberalized \(\delta\)-rule in free variable semantic tableaux ⋮ Tableau-based characterization and theorem proving for default logic ⋮ Locally Boolean spectra ⋮ Tableaus for many-valued modal logic ⋮ lean\(T^ AP\): Lean tableau-based deduction ⋮ The model evolution calculus as a first-order DPLL method ⋮ The complexity of concept languages ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Some techniques for proving termination of the hyperresolution calculus ⋮ The co-invariant generator: An aid in deriving loop bodies ⋮ Annual meeting of the Association for Symbolic Logic, Notre Dame, 1993 ⋮ Deontic Paradoxes and Tableau System for Kalinowski’s Deontic Logic K1 ⋮ On Skolemization in constrained logics ⋮ Intuitive minimal abduction in sequent calculi ⋮ A Correspondence Between Variable Relations And Three-Valued Propositional Logic ⋮ A semantics for reasoning consistently in the presence of inconsistency ⋮ Contraction-free sequent calculi for intuitionistic logic ⋮ A strict constrained superposition calculus for graphs ⋮ Rasiowa-Sikorski deduction systems with the rule of cut: a case study ⋮ Prime forms and minimal change in propositional belief bases ⋮ Dual erotetic calculi and the minimal \(\mathsf{LFI}\) ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Herbrand's fundamental theorem in the eyes of Jean van Heijenoort ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ Analytic tableaux for default logics ⋮ A Tableaux System for Deontic Action Logic ⋮ A fast saturation strategy for set-theoretic tableaux ⋮ Subgoal alternation in model elimination ⋮ Proving correctness of labeled transition systems by semantic tableaux ⋮ ileanTAP: An intuitionistic theorem prover ⋮ A sequent calculus for reasoning in four-valued Description Logics ⋮ Unnamed Item ⋮ A tableau calculus for first-order branching time logic ⋮ First-order dialogical games and tableaux ⋮ On Height and Happiness ⋮ Congruence Closure with Free Variables ⋮ Niche width theory reappraised ⋮ Incremental theory reasoning methods for semantic tableaux ⋮ The disconnection method ⋮ A tableau calculus for minimal model reasoning ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ Grammar specification in categorial logics and theorem proving ⋮ Graded tableaux for Rational Pavelka Logic ⋮ Self-verifying axiom systems, the incompleteness theorem and related reflection principles ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Theorem proving techniques for view deletion in databases ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ A general criterion for avoiding infinite unfolding during partial deduction ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ Automating most parts of hardware proofs in HOL ⋮ Verifying properties of HMS machine specifications of real-time systems ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Tableaux and dual tableaux: transformation of proofs ⋮ Fault-Tolerant Aggregate Signatures ⋮ Analytica -- an experiment in combining theorem proving and symbolic computation ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ Model elimination without contrapositives ⋮ Semantic tableaux with ordering restrictions ⋮ LeanT A P: Lean tableau-based theorem proving ⋮ Reasoning about System-Degradation and Fault-Recovery with Deontic Logic ⋮ How true it is = who says it's true ⋮ Unnamed Item ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ An exploration of the partial respects in which an axiom system recognizing solely addition as a total function can verify its own consistency ⋮ Human-centered automated proof search ⋮ Hyper tableaux ⋮ What you always wanted to know about rigid E-unification ⋮ A modal action logic based framework for organization specification and analysis ⋮ An abductive framework for negation in disjunctive logic programming ⋮ Simplification of boolean verification conditions ⋮ Functional Completeness in CPL via Correspondence Analysis ⋮ The Method of Socratic Proofs Meets Correspondence Analysis ⋮ Correspondences between classical, intuitionistic and uniform provability ⋮ Constructing infinite models represented by tree automata ⋮ Automated Model Building: From Finite to Infinite Models ⋮ Using tableaux to automate the Lambek and other categorial calculi ⋮ A proof procedure for the logic of hereditary Harrop formulas ⋮ Gentzen-type systems, resolution and tableaux ⋮ \textsf{Goéland}: a concurrent tableau-based theorem prover (system description) ⋮ Adding a temporal dimension to a logic system ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I

This page was built for publication: