- Related Sites
- Encyclopedia Entries
- Stanford Encyclopedia of Philosophy
- Category Theory
- Computability and Complexity
- Computation in Physical Systems
- Computational Complexity Theory
- Computer and Information Ethics
- Computing and Moral Responsibility
- Information
- The Lambda Calculus
- Logic and Artificial Intelligence
- Philosophy of Computer Science
- Philosophy of Mathematics
- Philosophy of Technology
- Recursive Functions
- Semantic Conceptions of Information
- Set Theory
- Internet Encyclopedia of Philosophy
- Wikipedia
- Stanford Encyclopedia of Philosophy
- Bibliographies
- Books
- Ontology of Philosophy of Computer Science
- Blogs
- Organizations and Societies
- Conferences and Symposia
- Logic
- An Automated Modal Reasoner
- Arend Theorem Prover
- Argdown
- Carnap
- Conan- A proof editor for first order logic
- Coq Proof Assistant
- GAPT: General Architecture for Proof Theory
- List of Computational Tools for Modal Logic
- Logic Matters
- Microsoft's Lean
- Open Logic Project
- Proof General
- SymPy Logic Module
- Taut
- Programming Languages and Libraries
- Digital Philosophy
- University Departments and Research Centers
- Magazines and Newsletters
- Individual Philosophers
- Philosophical Networks
- Software for Philosophers
- Textbooks (not free)
A curated list of awesome resources that bridge Philosophy and Computer Science. Last update: 2023-11-25
"The aim of this website is to highlight the many strong links between Philosophy and Computing, for the benefit of students (and potential students) of both disciplines:…"
- Abductive logic programming
- Answer set programming
- Concurrent logic programming
- Inductive logic programming
A review of Logic Courseware and free and open access texts at Daily Nous
“Category Theory, Haskell, Concurrency, C++”
Formal methods, including TLA+ and Alloy.
"A group blog on math, physics and philosophy". There is an associated wiki. “The nLab is a collaborative wiki. It grew out of the desire (I, II) to have a place for development (the ’Lab’ in ’nLab’) and indexed archives of the ideas and concepts surrounding the discussions at the The n-Category Café. These discussions primarily are about mathematics, physics and philosophy from the perspective of category theory and higher category theory (the ’n’ in ’nLab’ and nPOV).“
"This program takes lists of formalized sentences and checks them for consistency or validity in Propositional Modal Logic (S5 Axiom System)." Created by Brian Tackett.
‘Arend implements a version of homotopy type theory with an interval type, which syntax is similar to cubical type theory. This implies several nice properties of path types and allows for a simple and clean definition of higher inductive types (including recursive ones).’
A variation of markdown that allows one to create argument maps.
"Carnap is a free and open software framework written in Haskell for teaching and studying formal logic." An introductory blog post by the author, Graham Leach-Krouse at Daily Nous.
Conan- A proof editor for first order logic
Written in OCaml, "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching."
Home page of Wiki
‘GAPT is a proof theory framework developed primarily at the Vienna University of Technology. GAPT contains data structures, algorithms, parsers and other components common in proof theory and automated deduction. In contrast to automated and interactive theorem provers whose focus is the construction of proofs, GAPT concentrates on the transformation and further processing of proofs.’
"Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs."
"Proof General is a generic interface for proof assistants (also known as interactive theorem provers), based on the extensible, customizable text editor Emacs." Since I'm an Emacs user, this has strong appeal.
"The logic module for SymPy allows to form and manipulate logic expressions using symbolic and Boolean values."
"This is a website that contains randomly-generated, self-correcting logic excercises. It runs directly on your browser, so there is no need to download anything. It was designed by Ariel Roffé (UBA / UNQ / CONICET), with support from the BA-Logic group"
‘Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.’
"miniKanren is an embedded Domain Specific Language for logic programming."
"miniKanren has been implemented in a growing number of host languages, including Scheme, Racket, Clojure, Haskell, Python, JavaScript, Scala, Ruby, OCaml, and PHP, among many other languages."
-
"If you think the greatest pleasure in programming comes from getting a lot done with code that simply and clearly expresses your intention, then programming in Common Lisp is likely to be about the most fun you can have with a computer. You'll get more done, faster, using it than you would using pretty much any other language."
‘We present Logica, a novel open source Logic Programming language. A successor to Yedalog (a language developed at Google earlier) it is a Datalog-like logic programming language. Logica code compiles to SQL and runs on Google BigQuery (with experimental support for PostgreSQL and SQLite), but it is much more concise and supports the clean and reusable abstraction mechanisms that SQL lacks. It supports modules and imports, it can be used from an interactive Python notebook and it even makes testing your queries natural and easy.’
A GitHub repository of Prolog awesomeness.
‘Metagol is an inductive logic programming (ILP) system based on meta-interpretive learning. Metagol is written in Prolog and runs with SWI-Prolog.’
'An ergonomic, mobile-first, Prolog playground!'
"PrologHub is dedicated to bringing together the Prolog community to share ideas and knowledge. Our aim is to encourage the growth and development of the community."
‘Picat is a simple, and yet powerful, logic-based multi-paradigm programming language aimed for general-purpose applications.’
"Logic Programming in Python"
"PySWIP is a Python - SWI-Prolog bridge enabling to query SWI-Prolog in your Python programs. It features an (incomplete) SWI-Prolog foreign language interface, a utility class that makes it easy querying with Prolog and also a Pythonic interface."
tt (truth table) is a library aiming to provide a Pythonic toolkit for working with Boolean expressions and truth tables.
"My work applies visualization and network science to humanities datasets, especially the history of philosophy. I also write on digital humanities and the politics of technology."
A comprehensive map of all influential relationships in philosophy according to Wikipedia.
Created by Torin Doppelt
Accompanying blog to Spinoza's Ethics 2.0
This is a presentation by Lisa Spirohttps://digitalscholarship.wordpress.com)
"For the purposes of ACM Transactions on Computational Logic, the field of computational logic consists of all uses of logic in computer science."
Newsletter on Philosophy and Computers - American Philosophical Association
John is the creator of Pandoc.
Contributed by Moses Boudorides, a series of Jupyter notebooks showing sentence-co-occurring relationships among concepts. Works analyzed include Heidegger's "The Question Concerning Technology" and Nietzsche's "Thus Spake Zarathustra".
An iOS app for creating argument maps.
"Personal philosophy database software," created by Jason Winning.