On Matrices with Connections
From MaRDI portal
Publication:3922205
DOI10.1145/322276.322277zbMath0468.68097MaRDI QIDQ3922205
Publication date: 1981
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322276.322277
03B35: Mechanization of proofs and logical operations
Related Items
A logical framework for depiction and image interpretation, Linearity and regularity with negation normal form, The disconnection tableau calculus, On connections and higher-order logic, 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, Towards a unified model of search in theorem-proving: subgoal-reduction strategies
