has a link to a discussion of some early Skolem machine
software prototypes using Prolog and Java.
Historial note (c.2007): §6.1 of The Prolog Tutorial ↬
Skolem Machines, Fundamenta Informaticae, 91 (1) 2009, pp.79-103
J.Fisher, ↬ QEDF search procedure defined, technote, 2009 (modified 2010-2012). A queueing technique for generative rules was suggest by Marc Bezem and implemented for colog. This search completeness method predates the invention of the distributed choices algortithm which was implemented in 2014.
J.Fisher, ↬ Guarded Coherent Logic Domains, technote, Summer 2009 .
J.Fisher, ↬ Coalgebra dynamics for Skolem Machine Computations> , technote, Fall 2010.
Andrew Polonsky and Marc Bezem, ↬ Proof Objects for Logical Translations, The 1st Coq Workshop Proceedings, Hugo Herbelin (Ed.) August 09, pages 49-60.
Andrew Polonsky, ↬ Proofs, Types, and Lambda Calculus, Doctoral Thesis, UiB, December 10, 2010.
Bjarne Holen, Dag Hovland , and Martin Giese, ↬ Efficient Rule-Matching for Automated Coherent Logic, (NIK-2013 conference paper, Google post)
Thierry Coquand and Nils Anders Danielsson,↬ Isomorphism is equality. Indagationes Mathematicae 24(4):1105–1120, 2013, doi:10.1016/j.indag.2013.09.002. {This paper has a nice approach to showing univalence in a De Bruijn motivated logic/type system. Automating the proof in this paper using an Autolog program would make an excellent future project ...}
S.Stojanovic, J.Narboux, M.Bezem, P. Janicic, ↬ A Vernacular for Coherent Logic (ResearchGate post)
Roy Dyckhoff and Sara Negri, Geometrisation of first-order logic, Bulletin of Symbolic Logic 21, pp 123-163, 2015.
↬ st-andrews link... See also (2021-): https://en.wikipedia.org/wiki/Geometric_logic/a>
Salman Sagha, A Framework for Exploring Finite Models, Dissertation, WORCESTER POLYTECHNIC INSTITUTE, May 2015.
Roy Dyckhoff, Intuitionistic decision procedures since Gentzen, in Advances in Proof Theory, Volume 28 of the series Progress in Computer Science and Applied Logic pp 245-267, 05 May 2016.
Marc Bezem, "Elements of Mathematics" in the Digital Age by Marc Bezem (Universitetet i Bergen, Norway).
This YouTube presentation discusses historical background for automatic proving or checking of mathematical/logical results, and some future prospects. FOMUS 2016 -- Published on Apr 2, 2017. (Bezem gave an earlier version of this talk in spring 2014 at Cal Poly Pomona Computer Science department.)
Irving H. Anellis, Francine Abeles, The Historical Sources of Tree Graphs and the Tree Method in the Work of Peirce and Gentzen , ResearchGate posting.
The motivation for the name AutoLog comes from Nicolaas Govert de Bruijn 's AutoMath language/project.
It is intended that AutoLog eventually be a flexible extended coherent logic programming language suitable for computation by some Skolem Machine. (Automath checks its mathematical input for correct specification.)
Bezem, Marc & Buchholtz, Ulrik & Coquand, Thierry. (2017). Syntactic Forcing Models for Coherent Logic. ↬ https://www.researchgate.net/publication/321994326_Syntactic_Forcing_Models_for_Coherent_Logic
AutoLog Development webpage
Follow the link cited in the Autolog Design Notebook.
Autolog (Skolem Machine) inference computation mechanisms are related to infinitary rewriting and infinitary equational (modulator) logic. Proof search is potentially infinitary and terminal via tactics. Following is an astute theoretical reference for this aspect of things.Jorg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, Alexandra Silva,
Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
Logical Methods in Computer Science, Vol. 14(1:3)2018, pp.1-44.
Carsten Butz, Regular Categories and Regular Logic, BRICS Lecture Series, LS-98-2, October 1998.
See nlab pages re: regular category, coherent category.
Project assignment: express regular/coherent category theory in autolog (See 4metaCAT ...)
Marc Bezem, Thierry Coquand, Skolem's Theorem in Coherent Logic, Fundamenta Informaticae 167 (2019) 1-14.
coherent cogic in nlab (since 2009), https://ncatlab.org/nlab/show/coherent+logic.
Marc Bezem's github repository, Coherent Logic at Proof and Computation, 2022
Examples regarding the interplay between disjuction and rule order for colog14I (8/1/2023)