Man-machine theorem proving in graph theory

DOI10.1016/0004-3702(88)90030-6zbMATH Open0646.68107OpenAlexW1965876066MaRDI QIDQ1104124FDOQ1104124

Authors Irena Pevac, Dragoš Cvetković

Publication date 1988

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0004-3702(88)90030-6

zbMATH Keywords

interactive programmingcomplexity measurecomputerized graph theory bibliographygraph theoretic algorithmsmechanical theorem prover

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Software, source code, etc. for problems pertaining to combinatorics (05-04)

Recommendations

• scientific article; zbMATH DE number 3906548
• scientific article; zbMATH DE number 4047184
• scientific article; zbMATH DE number 4101136
• scientific article; zbMATH DE number 3845636
• Computer theorem proving in mathematics
• Deduction graphs: an algorithm and applications
• scientific article; zbMATH DE number 1748578
• Computability of graphs
• scientific article; zbMATH DE number 4128857

Cites work

• scientific article; zbMATH DE number 3845636 (Why is no real title available?)
• scientific article; zbMATH DE number 3864540 (Why is no real title available?)
• scientific article; zbMATH DE number 3814998 (Why is no real title available?)
• scientific article; zbMATH DE number 3825879 (Why is no real title available?)
• scientific article; zbMATH DE number 3906548 (Why is no real title available?)
• scientific article; zbMATH DE number 3938595 (Why is no real title available?)
• scientific article; zbMATH DE number 3684928 (Why is no real title available?)
• scientific article; zbMATH DE number 3733991 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• A man-machine theorem-proving system
• Graph equations for line graphs and total graphs
• Non-resolution theorem proving
• Splitting and reduction heuristics in automatic theorem proving
• Theorem proving with abstraction

Cited in

(19)

• Variable neighborhood search for extremal graphs. V: Three ways to automate finding conjectures
• Automated conjectures on upper bounds for the largest Laplacian eigenvalue of graphs
• Computers and discovery in algebraic graph theory
• On graphs whose second largest eigenvalue does not exceed \((\sqrt {5}-1)/2\)
• Bounds and conjectures for the signless Laplacian index of graphs
• scientific article; zbMATH DE number 3970135 (Why is no real title available?)
• scientific article; zbMATH DE number 3938595 (Why is no real title available?)
• \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
• scientific article; zbMATH DE number 3870636 (Why is no real title available?)
• Gazing: An approach to the problem of definition and lemma use
• scientific article; zbMATH DE number 3952769 (Why is no real title available?)
• Star partitions and the graph isomorphism problem
• A survey of automated conjectures in spectral graph theory
• Representations of graphs and networks (coding, layouts and embeddings)
• A knowledge-based system for graph theory demonstrated by partial proofs for graph-colouring problems
• Operational research models in action, the result of international cooperation -- a potpourri
• scientific article; zbMATH DE number 3845636 (Why is no real title available?)
• scientific article; zbMATH DE number 3906548 (Why is no real title available?)
• scientific article; zbMATH DE number 4081618 (Why is no real title available?)

Describes a project that uses

Uses Software

• AFFIRM

This page was built for publication: Man-machine theorem proving in graph theory

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