On Matrices with Connections

Cited in

(35)

Automated theorem proving methods
A new reduction rule for the connection graph proof procedure
Reduction rules for resolution-based systems
A new subsumption method in the connection graph proof procedure
A kind of logical compilation for knowledge bases
Controlled integration of the cut rule into connection tableau calculi
On the termination of clause graph resolution
Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system
Connection methods in linear logic and proof nets construction
Proof-search in type-theoretic languages: An introduction
A comparative study of several proof procedures
A uniform procedure for converting matrix proofs into sequent-style systems
A typed resolution principle for deduction with conditional typing theory
Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
Knowledge-based proof planning
Set of support, demodulation, paramodulation: a historical perspective
ABox abduction in the description logic \(\mathcal{ALC}\)
Towards a unified model of search in theorem-proving: subgoal-reduction strategies
T-string unification: unifying prefixes in non-classical proof methods
Proof-terms for classical and intuitionistic resolution
Converting non-classical matrix proofs into sequent-style systems
A tableau method for the Lambek calculus based on a matrix characterization
From Schütte’s Formal Systems to Modern Automated Deduction
scientific article; zbMATH DE number 7204450 (Why is no real title available?)
Compressing propositional refutations
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
Connection-based proof construction in linear logic
What you always wanted to know about rigid \(E\)-unification
A logical framework for depiction and image interpretation
On structures of regular standard contradictions in propositional logic
Simultaneous rigid E-unification is undecidable
On structures of sign-boundary and diagonal vacancy-type standard contradictions
Linearity and regularity with negation normal form
The disconnection tableau calculus
On connections and higher-order logic

This page was built for publication: On Matrices with Connections

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3922205)