scientific article; zbMATH DE number 3568056

Cited in

(only showing first 100 items - show all)

Using forcing to prove completeness of resolution and paramodulation
A Prolog technology theorem prover: Implementation by an extended Prolog compiler
Compiling a default reasoning system into Prolog
An order-sorted logic for knowledge representation systems
Exact Max-SAT solvers for over-constrained problems
A utility-valued logic for decision making
How good are branching rules in DPLL?
An implementation of Kripke-Kleene semantics
Mode-Directed Inverse Entailment for Full Clausal Theories
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
Branch-and-cut solution of inference problems in propositional logic
A simplified problem reduction format
Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
Goal directed strategies for paramodulation
An efficient solver for weighted Max-SAT
A Noetherian and confluent rewrite system for idempotent semigroups
Strategies for modal resolution: Results and problems
Subsumption and implication
About the Paterson-Wegman linear unification algorithm
Linear resolution for consequence finding
Semi-intelligible Isar proofs from machine-generated proofs
Closures and fairness in the semantics of programming logic
Clause trees: A tool for understanding and implementing resolution in automated reasoning
Term rewriting: Some experimental results
Negation as failure: careful closure procedure
Approximating minimal unsatisfiable subformulae by means of adaptive core search
Branching rules for satisfiability
Defining answer classes using resolution refutation
An efficient algorithm for the 3-satisfiability problem
Implication of clauses is undecidable
A practically efficient and almost linear unification algorithm
Fuzzy logic programming
First order LUB approximations: characterization and algorithms
Partition-based logical reasoning for first-order and propositional theories
Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
Some results and experiments in programming techniques for propositional logic
A structure-preserving clause form translation
A relevance restriction strategy for automated deduction
SATCHMORE: SATCHMO with RElevancy
The \(Multi\)-SAT algorithm
Controlled integration of the cut rule into connection tableau calculi
Theorem-proving with resolution and superposition
Resolution vs. cutting plane solution of inference problems: Some computational experience
Linear programs for constraint satisfaction problems
Combining instance generation and resolution
Efficient solution of linear diophantine equations
Embedding circumscriptive theories in general disjunctive programs
Embedding complex decision procedures inside an interactive theorem prover.
A parallel approach for theorem proving in propositional logic
Parsing as non-Horn deduction
Logic applied to integer programming and integer programming applied to logic
Meta-resolution: An algorithmic formalisation
Tractable reasoning via approximation
Solving propositional satisfiability problems
Representing and building models for decidable subclasses of equational clausal logic
Some techniques for proving termination of the hyperresolution calculus
A Prolog technology theorem prover: A new exposition and implementation in Prolog
Recursive query processing: The power of logic
A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
Removing redundancy from a clause
Hierarchical deduction
A new algorithm for the propositional satisfiability problem
Producing and verifying extremely large propositional refutations
Linearity and regularity with negation normal form
The search efficiency of theorem proving strategies
Prolog technology for default reasoning: proof theory and compilation techniques
Gentzen-type systems, resolution and tableaux
Complexity of resolution proofs and function introduction
The achievement of knowledge bases by cycle search.
A general framework to build contextual cover set induction provers
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Knowledge-based proof planning
Generalized subsumption and its applications to induction and redundancy
Unification theory
Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
Learning action models from plan examples using weighted MAX-SAT
A weight-balanced branching rule for SAT
Uniform and non uniform strategies for tableaux calculi for modal logics
A superposition oriented theorem prover
Unification in a combination of arbitrary disjoint equational theories
scientific article; zbMATH DE number 7680806 (Why is no real title available?)
\(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\)
Semantics of Horn and disjunctive logic programs
Building proofs or counterexamples by analogy in a resolution framework
Craig interpolation with clausal first-order tableaux
An automatic proof of Gödel's incompleteness theorem
On preprocessing techniques and their impact on propositional model counting
A resolution principle for constrained logics
1998–99 Annual Meeting of the Association for Symbolic Logic
HyperMonitor: a Python prototype for hyper predictive runtime verification
A theorem prover for a computational logic
Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
Modeling production rules by means of predicate transition networks
Connection calculus theorem proving with multiple built-in theories
\(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
Propositional calculus problems in CHIP
Extracting models from clause sets saturated under semantic refinements of the resolution rule.
ABox abduction in the description logic \(\mathcal{ALC}\)
Local simplification
Investigations into proof structures

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 Q4139711)