scientific article; zbMATH DE number 3415409
From MaRDI portal
Publication:5679729
Cited in
(only showing first 100 items - show all)- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- A simple deduction method for modal logic
- Equational methods in first order predicate calculus
- Maximal unifiable subsets and minimal non-unifiable subsets
- Complete problems in the first-order predicate calculus
- Completeness results for inequality provers
- Inferences for numerical dependencies
- On solving the equality problem in theories defined by Horn clauses
- Multi-layer logic - a predicate logic including data structure as knowledge representation language
- A structure-preserving clause form translation
- Hierarchical deduction
- Resolution on formula-trees
- Rewrite method for theorem proving in first order theory with equality
- Inconsistency check of a set of clauses using Petri net reductions
- The number of proof lines and the size of proofs in first order logic
- History and basic features of the critical-pair/completion procedure
- About the Paterson-Wegman linear unification algorithm
- Implication of clauses is undecidable
- A new reduction rule for the connection graph proof procedure
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- An algorithm to compute circumscription
- Optimizing propositional calculus formulas with regard to questions of deducibility
- Modal resolution in clausal form
- A note on the completeness of resolution without self-resolution
- Finite approximatization of languages for representation of system properties: Axiomatization of dependencies
- Purging in an equality data base
- Theorem proving with abstraction
- An extension to linear resolution with selection function
- Experiments with resolution-based theorem-proving algorithms
- A simplified problem reduction format
- An analysis of loop checking mechanisms for logic programs
- Resolution for some first-order modal systems
- The contraction rule and decision problems for logics without structural rules
- Reduction rules for resolution-based systems
- Tautologies and positive solvability of linear homogeneous systems
- An order-sorted logic for knowledge representation systems
- Free fuzzy groups and fuzzy group presentations
- A new subsumption method in the connection graph proof procedure
- Linear resolution for consequence finding
- On the relations between stable and well-founded semantics of logic programs
- The completeness of gp-resolution for annotated logics
- An implementation of hyper-resolution
- A partial evaluator, and its use as a programming tool
- Complete problems for deterministic polynomial time
- Non-resolution theorem proving
- Complete demodulation for automatic theorem proving
- On an unsatisfiability-satisfiability prover
- Decomposition of linguistic-logical decision models in distributed computing environments
- Theorem proving by chain resolution
- Prolog technology for default reasoning: proof theory and compilation techniques
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Universal abstract consistency class and universal refutation
- Free fuzzy modules and their bases
- Completeness issues in RUE-NRF deduction: The undecidability of viability
- Gentzen-type systems, resolution and tableaux
- Fuzzy operator logic and fuzzy resolution
- Automated theorem proving in temporal logic: T-resolution
- A derived algorithm for evaluating -expressions over abstract sets
- On the mechanical derivation of loop invariants
- A resolution principle for constrained logics
- Hybrid reasoning using universal attachment
- Some results on the containment and minimization of (in)equality queries
- A logic-based approach to query processing in federated databases
- The rue theorem-proving system: The complete set of LIM+ challenge problems
- Problem solving by searching for models with a theorem prover
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Ordered model trees: A normal form for disjunctive deductive databases
- Enumeration of success patterns in logic programs
- An average case analysis of a resolution principle algorithm in mechanical theorem proving.
- Polynomial-time inference of all valid implications for Horn and related formulae
- On renamable Horn and generalized Horn functions
- Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system
- Solving problems with automated reasoning, expert systems and neural networks
- A formal specification of document processing
- On Skolemization in constrained logics
- A temporal logic for real-time partial ordering with named transactions
- Probabilistic conflicts in a search algorithm for estimating posterior probabilities in Bayesian networks
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Computing answers with model elimination
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- A fuzzy logic with interval truth values
- Deciding the E^+-class by an a posteriori, liftable order
- Linear strategy for Boolean ring based theorem proving
- Proofs as schemas and their heuristic use
- Automatic synthesis of logical models for order-sorted first-order theories
- Formalization of the resolution calculus for first-order logic
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- The reference ontology of collective behavior of autonomous agents and its extensions
- On ultrafilter logic and special functions
- A resolution-based system for symbolic approximate reasoning
- Logic inference using formulas with temporal connectives
- Inherited extension of many-sorted theories
- P-Prolog: A parallel logic language based on exclusive relation
- Horn equational theories and paramodulation
- On equational theories, unification, and (un)decidability
- The linked conjunct method for automatic deduction and related search techniques
- A method for the synthesis of deducibility conditions for Horn and some other formulas
- The achievement of knowledge bases by cycle search.
- Working with ARMs: Complexity results on atomic representations of Herbrand models
- The application of automated reasoning to formal models of combinatorial optimization
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 Q5679729)
