Pages that link to "Item:Q5514129"
From MaRDI portal
The following pages link to A Machine-Oriented Logic Based on the Resolution Principle (Q5514129):
Displaying 50 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Evidence algorithm and inference search in first-order logics (Q286802) (← links)
- Unification for infinite sets of equations between finite terms (Q287056) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Correia semantics revisited (Q300562) (← links)
- Invariant-free clausal temporal resolution (Q352974) (← links)
- Learning from conflicts in propositional satisfiability (Q427560) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- Dealing with satisfiability and \(n\)-ary CSPs in a logical framework (Q438582) (← links)
- An introduction to mechanized reasoning (Q504394) (← links)
- Enhancing unsatisfiable cores for LTL with information on temporal relevance (Q507378) (← links)
- Prominent classes of the most general subsumptive solutions of Boolean equations (Q507645) (← links)
- An approach to completing variable names for implicitly typed functional languages (Q526448) (← links)
- A calculus for automatic verification of Petri nets based on resolution and dynamic logics (Q530854) (← links)
- John McCarthy's legacy (Q543573) (← links)
- On the power of clause-learning SAT solvers as resolution engines (Q543613) (← links)
- Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) (Q545319) (← links)
- The correctness of Newman's typability algorithm and some of its extensions (Q549191) (← links)
- A sound and complete model-generation procedure for consistent and confidentiality-preserving databases (Q549726) (← links)
- On the complexity of cutting-plane proofs (Q580175) (← links)
- An experimental logic based on the fundamental deduction principle (Q580998) (← links)
- Unification in Boolean rings and Abelian groups (Q582073) (← links)
- An almost linear Robinson unification algorithm (Q582141) (← links)
- Order-sorted unification (Q582269) (← links)
- Unification in a combination of arbitrary disjoint equational theories (Q582270) (← links)
- Extracting the resolution algorithm from a completeness proof for the propositional calculus (Q636273) (← links)
- Best unifiers in transitive modal logics (Q647403) (← links)
- Algorithms for generating arguments and counterarguments in propositional logic (Q648354) (← links)
- Linearity and iterator types for Gödel's system \(\mathcal T\) (Q656851) (← links)
- Meta-resolution: An algorithmic formalisation (Q671650) (← links)
- Lazy narrowing: strong completeness and eager variable elimination (Q671677) (← links)
- Resolution search (Q674925) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Average-case analysis of unification algorithms (Q685442) (← links)
- An essay on resolution logics (Q687163) (← links)
- Parsing as non-Horn deduction (Q688151) (← links)
- Cut formulas in propositional logic (Q689298) (← links)
- Enhancing global SLS-resolution with loop cutting and tabling mechanisms (Q703484) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- On the parameterized complexity of associative and commutative unification (Q729894) (← links)
- Regular expression order-sorted unification and matching (Q741252) (← links)
- Automation methods for logical derivation and their application in the control of dynamic and intelligent systems (Q742012) (← links)
- Clausal presentation of theories in deduction modulo (Q744331) (← links)
- Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics (Q744990) (← links)
- A practical unification algorithm (Q751312) (← links)
- Using forcing to prove completeness of resolution and paramodulation (Q757093) (← links)
- Theorem-proving with resolution and superposition (Q757094) (← links)
- A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains (Q759491) (← links)
- \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic (Q778417) (← links)
- Grammatical unification (Q789185) (← links)
