scientific article; zbMATH DE number 46359
From MaRDI portal
Publication:3996619
Recommendations
- scientific article; zbMATH DE number 837700
- scientific article; zbMATH DE number 1070624
- scientific article; zbMATH DE number 1751350
- Proof theory and automated deduction
- First-order theorem proving: foreword
- scientific article; zbMATH DE number 1300967
- scientific article; zbMATH DE number 3976991
- Automatic models of first order theories
- Theorem Proving in Higher Order Logics
- First-order logic theorem proving and model building via approximation and instantiation
Cited in
(only showing first 100 items - show all)- Automatic models of first order theories
- scientific article; zbMATH DE number 4043814 (Why is no real title available?)
- Hyper tableaux
- A Correspondence Between Variable Relations And Three-Valued Propositional Logic
- Functional Completeness in CPL via Correspondence Analysis
- Analytic tableaux for default logics
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
- Intuitive minimal abduction in sequent calculi
- Using tableaux to automate the Lambek and other categorial calculi
- Gentzen-type systems, resolution and tableaux
- An algorithm for automatic demonstration of logical theorems
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- A tableau calculus for minimal model reasoning
- scientific article; zbMATH DE number 1507179 (Why is no real title available?)
- Locally Boolean spectra
- Tableaux and dual tableaux: transformation of proofs
- Analytica -- an experiment in combining theorem proving and symbolic computation
- A tableau calculus for first-order branching time logic
- A general criterion for avoiding infinite unfolding during partial deduction
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Model elimination without contrapositives
- First-order dialogical games and tableaux
- A modal action logic based framework for organization specification and analysis
- Theorem proving techniques for view deletion in databases
- How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic q
- A sequent calculus for reasoning in four-valued description logics
- The disconnection method
- The blossom of finite semantic trees
- AVATAR: The Architecture for First-Order Theorem Provers
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
- scientific article; zbMATH DE number 4114588 (Why is no real title available?)
- The complexity of concept languages
- First-order theorem proving: foreword
- scientific article; zbMATH DE number 195157 (Why is no real title available?)
- A semantics for reasoning consistently in the presence of inconsistency
- scientific article; zbMATH DE number 3976991 (Why is no real title available?)
- scientific article; zbMATH DE number 837700 (Why is no real title available?)
- Fault-tolerant aggregate signatures
- Contraction-free sequent calculi for intuitionistic logic
- \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
- A logic of separating modalities
- Herbrand's fundamental theorem in the eyes of Jean van Heijenoort
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
- A fast saturation strategy for set-theoretic tableaux
- Congruence closure with free variables
- The method of Socratic proofs meets correspondence analysis
- Theorem Proving in Higher Order Logics
- Deontic paradoxes and tableau system for Kalinowski's deontic logic \(K1\)
- Superposition theorem proving for abelian groups represented as integer modules
- What you always wanted to know about rigid \(E\)-unification
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Formalized proof systems for propositional logic
- A generic deskolemization strategy
- Automated deduction
- Self-verifying axiom systems, the incompleteness theorem and related reflection principles
- Model building with ordered resolution: Extracting models from saturated clause sets
- The liberalized -rule in free variable semantic tableaux
- The co-invariant generator: An aid in deriving loop bodies
- How true it is = who says it's true
- Correspondences between classical, intuitionistic and uniform provability
- scientific article; zbMATH DE number 4056963 (Why is no real title available?)
- Adding a temporal dimension to a logic system
- A strict constrained superposition calculus for graphs
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- Human-centered automated proof search
- Constructing infinite models represented by tree automata
- Prime forms and minimal change in propositional belief bases
- Dual erotetic calculi and the minimal \(\mathsf{LFI}\)
- Superposition theorem proving for abelian groups represented as integer modules
- An abductive framework for negation in disjunctive logic programming
- Annual meeting of the Association for Symbolic Logic, Notre Dame, 1993
- An exploration of the partial respects in which an axiom system recognizing solely addition as a total function can verify its own consistency
- Automated Model Building: From Finite to Infinite Models
- Rasiowa-Sikorski deduction systems with the rule of cut: a case study
- A Tableaux System for Deontic Action Logic
- On the relative merits of path dissolution and the method of analytic tableaux
- Accelerating tableaux proofs using compact representations
- Grammar specification in categorial logics and theorem proving
- scientific article; zbMATH DE number 708485 (Why is no real title available?)
- A proof procedure for the logic of hereditary Harrop formulas
- Specification and Verification of Multi-Agent Systems
- On height and happiness
- LeanT A P: Lean tableau-based theorem proving
- Structuring and automating hardware proofs in a higher-order theorem- proving environment
- The model evolution calculus as a first-order DPLL method
- Proving correctness of labeled transition systems by semantic tableaux
- The saturated tableaux for linear miniscope Horn-like temporal logic
- Subgoal alternation in model elimination
- Graded tableaux for Rational Pavelka Logic
- Specifying and verifying organizational security properties in first-order logic
- Automating most parts of hardware proofs in HOL
- Verifying properties of HMS machine specifications of real-time systems
- \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
- Reasoning about System-Degradation and Fault-Recovery with Deontic Logic
- Niche width theory reappraised
- Incremental theory reasoning methods for semantic tableaux
- Semantic tableaux with ordering restrictions
- scientific article; zbMATH DE number 1761887 (Why is no real title available?)
- A tableau prover for domain minimization
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 Q3996619)
