Practal — Practical Logic

A Bicycle for Your Mathematical Mind
Practal has its first monthly sponsor, many thanks to purebounce! 🎉
🆕 Recursive teXt
A new general-purpose text format.
🆕 Abstraction Logic
An exceptionally simple, yet revolutionary new foundation.
🆕 A First Look At Practal
The first release of Practal as a Visual Studio Code Extension is out!
Practal for VSCode
Pre-α Release

Practal in VSCode (Pre-α Release)

Would you like to know more?

Hi@practal.com
January 22, 2024 http://recursivetext.com Recursive teXt
Recursive teXt (RX) is a new general-purpose text format.
April 1, 2023 https://arxiv.org/abs/2304.00358 Logic is Algebra
Logic really is just algebra, given one uses the right kind of algebra, and the right kind of logic. The right kind of algebra is abstraction algebra, and the right kind of logic is abstraction logic.
February 5, 2023 https://practal.com/press/aair/1 Axioms Are Inference Rules
As it turns out, Abstraction Logic's axioms should be more general than initially thought. Instead of just terms, they should be inference rules.
February 4, 2023 https://practal.com/press/aflap/1 A First Look At Practal
The first release of Practal as a Visual Studio Code Extension is out! It is an early and experimental release without its most crucial functionality of proving and computing, but it has syntax highlighting and the ability to define your own syntax. It is already possible to state declarations, definitions and axioms, and definitions are properly checked.
July 13, 2022 https://arxiv.org/abs/2207.05610 Abstraction Logic: A New Foundation for (Computer) Mathematics
This was a submission to the CICM 2022 conference.
April 10, 2022 https://doi.org/10.47757/al.crete.1 Video: Abstraction Logic (UNILOG 2022)
This is a rerecording of a talk about Abstraction Logic at the UNILOG 2022 conference in Crete.
March 24, 2022 https://doi.org/10.47757/pwp.1 Indentation-Sensitive Parsing with Pyramids
This is a short note about combining indentation-sensitivity and pyramid grammars. We describe the syntax of indentation-sensitive pyramid grammars by one such grammar.
March 23, 2022 https://doi.org/10.47757/aal.1 Automating Abstraction Logic
We describe how to automate Abstraction Logic by translating it to the TPTP THF format.
December 21, 2021 (last revised December 23, 2021) https://doi.org/10.47757/pal.2 Philosophy of Abstraction Logic
Abstraction Logic has been introduced in a previous, rather technical article. In this article we take a step back and look at Abstraction Logic from a conceptual point of view. This will make it easier to appreciate the simplicity, elegance, and pragmatism of Abstraction Logic. We will argue that Abstraction Logic is the best logic for serving as a foundation of mathematics.
October 22, 2021 (last revised November 14, 2021) https://doi.org/10.47757/abstraction.logic.2 Abstraction Logic
Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.
July 29, 2021 https://doi.org/10.47757/practical.types.1 Practical Types
These are preliminary notes about Practal’s logic and its system of practical types. Practal Light is a research prototype implementing (part of) what is presented in this document.
July 17, 2021 https://doi.org/10.47757/practal.1 Practal — Practical Logic
This is a first sketch of the design of Practal, an interactive theorem proving system for practical logic.
May 18, 2021 https://doi.org/10.47757/obua.ll.1 A New Semantics for Local Lexing
A revised semantics for Local Lexing is presented that entirely avoids priority conflicts between non-empty tokens. Pyramid Grammars are introduced, and their semantics is given in terms of Local Lexing. It is demonstrated that they are more expressive than Context-Free Grammars, and at least as expressive as Parsing Expression Grammars.