My free and open-source research software^* tool, written in C++20, is meant to assist research in structural proof theory.

I made an effort to create an impressive README in GitHub-flavored Markdown — it turned out quite large. I am not worried about code quality but more about the project's perception as too complicated or messy.

I appreciate feedback and every star on GitHub.

There's also a mirror on Codeberg — but without forum functionality.

 
^{*It concerns a niche subject, but there are also undergraduate courses on logic for which it is already relevant — at some universities — so it is also educational software.}
 

Summary

pmGenerator can build, (exhaustively) collect and compress formal proofs for user-definable sets of axioms in Hilbert systems.

• The current 1.2.1 release supports two rules of inference:
  • D-rule: combines tree unification (on formulas) with modus ponens (⊢ψ,⊢ψ→φ ⇒ ⊢φ)
    
  • N-rule: necessitation (⊢ψ ⇒ ⊢□ψ), can optionally be enabled
• The project's readme also highlights several systems for which I generated (downloadable) collections of minimal proofs.
• I launched a proof minimization challenge as part of the project. For this one I am currently implementing an improved proof compression algorithm and preparing a large contribution (hopefully to be released within a few weeks from now), improving from currently 126171 to less than 29000 proof steps, which shows there is still quite some air for anyone who wishes to immortalize themselves in this mathematical challenge! :-)
• Questions, suggestions and remarks can be posted in the project's forum. I'd be especially happy to support new challengers.

One of the tool's simplest features is that it can parse D-proofs to print them in terms of formulas. For example, DD2D1D2DD2D1311 is a D-proof of 15 steps over three axioms, and ./pmGenerator -c -n -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp --parse DD2D1D2DD2D1311 -u results in

[0] DD2D1D2DD2D1311:
    1. 0→(¬0→0)  (1)
    2. ¬0→(¬1→¬0)  (1)
    3. (¬1→¬0)→(0→1)  (3)
    4. ((¬1→¬0)→(0→1))→(¬0→((¬1→¬0)→(0→1)))  (1)
    5. ¬0→((¬1→¬0)→(0→1))  (D):3,4
    6. (¬0→((¬1→¬0)→(0→1)))→((¬0→(¬1→¬0))→(¬0→(0→1)))  (2)
    7. (¬0→(¬1→¬0))→(¬0→(0→1))  (D):5,6
    8. ¬0→(0→1)  (D):2,7
    9. (¬0→(0→1))→((¬0→0)→(¬0→1))  (2)
    10. (¬0→0)→(¬0→1)  (D):8,9
    11. ((¬0→0)→(¬0→1))→(0→((¬0→0)→(¬0→1)))  (1)
    12. 0→((¬0→0)→(¬0→1))  (D):10,11
    13. (0→((¬0→0)→(¬0→1)))→((0→(¬0→0))→(0→(¬0→1)))  (2)
    14. (0→(¬0→0))→(0→(¬0→1))  (D):12,13
    15. 0→(¬0→1)  (D):1,14

where -c -n -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp means (1): 0→(1→0), (2): (0→(1→2))→((0→1)→(0→2)), and (3): (¬0→¬1)→(1→0) are configured as axioms (which are given in normal Polish notation).

There are many more features, e.g. to generate, search, reduce, convert, extract data, … there is a full list in the readme.

I'm currently in 1st year at my uni.. I'm not satisfied with the syllabus there, and feeling my time is being wasted. I, in my 1st sem completed C and C++ (having some very basic projects in C++), and want to explore mathematics with programming.. I asked ChatGPT, and it recommended me to start with Discrete Mathematics and suggested the book "Discrete Mathematics and Its Applications by K.H Rosen".. i searched for it and read that its not self-study friendly.. Can anyone guide me and also suggest me some better alternatives..

AFAIK the pattern community struggled to find a useful classification for patterns and tie them into an intuitive pattern language since its very birth. The GoF (creational, structural, behavioral) and POSA (architectural, design, idioms) classifications are too shallow to be of much use in practice.

Application of a structure-based classification (known as metapatterns) to architectural patterns results in an intuitive clusterization with patterns in each of 15-20 groups showing similarities in their properties and the problems they solve - as shown in the book below.

Links: short article with the theory, 300+ pages book (52 MB download).

That was the bright side of the story. The dark side is that I posted the book under the free CC BY license, and now publishers reject it because they cannot sell ebooks. I am left with the crazy (but working) idea, a compendium of a couple of hundred patterns - and no way to promote them. Any help is appreciated.

I’m interested in the topic and would like to explore it further. In school, we had a few classes on the philosophy of technology, which I really enjoyed. That’s why I’m wondering if there are any current, controversial topics that can already be discussed in depth without necessarily being an expert in the field and that are easily accessible to most people.

How can advances in algorithms, AI, or data science contribute to solving global environmental problems? Imagine coding a green future where technology powers renewable energy systems or reduces waste. Let’s share how computational thinking can push us toward an eco-friendly tech revolution.

Hey guys, I recently looked into the bit level representation of floats for a project, and I can see the reasoning behind pretty much all design choices made by IEEE, but the exponent bias just feels wrong, here is why:

1. The exponent bias was chosen to be 1-2^e_bits-1=-127 for float32 (-15 for float16, -1023 for float64), making the smallest biased exponent -126 and the largest 127 (since the smallest exponent is reserved for subnormals including 0, and the largest is for inf and nans).

2. The smallest possible fractional part is 1 and the largest is ≈2 (=2-2^-23) for normal numbers.

3. Because both the exponent range, and the fractionational range are biased upwards (from 1), this makes the smallest positive normal value 2^-14 and largest ≈2^16.

4. This makes the center (logarithmic scale) of positive mormal floats 2 instead of (the much more intuitive and unitary) 1, which is awful! (This also means that the median and also the geometric mean of positive normal values is 2 instead of 1).

This is true for all formats, but for the best intuitive understanding, let's look at what would happen if you had only two exponent bits: 00 -> subnormals including 0 01 -> normals in [1,2) 10 -> normals in [2,4) 11 -> inf and nans So the normals range from 1 to 4 instead 1/2 to 2, wtf!

Now let's look at what would change from updating the exponent shift to -2^e_bits-1:

1. The above mentioned midpoint would become 1 instead of 2 (for all floating point formats)

2. The exponent could be retrieved from its bit representation using the standard 2's complement method (instead of this weird "take the 2's complement and add 1" nonsense), this is used to represent signed integers pretty much everywhere.

3. We would get 2²³ new normal numbers close to zero AND increase the absolute precision of all 2²³ subnormals by an extra bit.

4. The maximum of finite numbers would go down from 3.4x10³⁸ to 1.7x10^38, but who cares, anyone in their right mind who's operating on numbers at that scale should be scared of bumping into infinity, and should scale down everything anyway. And still, we would create or increase the precision of exactly twice as many numbers near zero as we would lose above 10^38. Having some extra precision around zero would help a lot more applications then having a few extra values between 1.7x10³⁸ and 3.4x10^38.

Someone please convince me why IEEE's choice for the exponent bias makes sense, I can see the reasoning behind pretty much every other design choice, except for this and I would really like to think they had some nice justification for it.

Hi all, I feel like the problem I am working on has been already treated but I couldn't find GitHub or papers about. Could you help? Basically, I want to find a suboptimal path minimizing distances in graph. I know that I have to start from a given point and I know that I need to do M steps. If I have N points, M<<N. I don't care where I will finish, I just want to find an optimal route starting from point A and taking M steps, no problem in using heuristics cause computational cost is important.TSP makes me go back to origin and do M=N steps, so I guess I am looking at a modified Dijkstra? I need to implement in Python, someone knows anything helpful? Thanks a lot

Hi! I was wondering if theres any Theoretical Computer Science REU/Summer Research Programs that I could apply to? I've found very few and one of the deadlines already passed :( (I've applied to EPFL, missed ETH Zurich, have CAAR , OSU, ISTA, and DIMACS on my list)

Hello!

I spent the last week deep in claude/chatgpt-land building the most comprehensive curriculum I could for learning. Like a lot of folks I got into coding with only a little CS in school (minor in IT 20 years ago), and I've always wanted to learn more.

The goal with this is to provide:
1. Structured learning for anyone (feel free to ignore the suggested time per section)
2. A choose-your-own-adventure style approach (it can be taken in order or if you're familiar with areas slice off what you want to learn)
3. Several types of resources - I tried my best to find YouTube, paid courses, free courses, books, blogs, and podcasts for each area
4. Projects for each area, so you can actually demonstrate knowledge by building things (learn by doing!!)
5. Assessments for each area, so you can see if there are any gaps in your knowledge when you finish

I am 100% open to any feedback on this - whether on the overall structure or the actual content itself in any area. My hope is that this grows over time as people find better resources and this can be a living document.

https://github.com/nickfredman/cs-curriculum

I have to traverse a graph from given start to end node and find all distinct paths that happen to exist. There are ~2000 nodes in the graph.
FYI: I'm implementing the solution in python (DFS backtracking). However, it either fails to fetch or truncates or skips some values. How do I solve this?

The graph also has multiple edges going from anywhere to anywhere including cycles.

I have finished my bachelor's in Computer Science and I want to write a research paper. However, I am no longer affiliated with a university, so I’m unsure how to proceed. Can someone guide me through the process of writing and publishing a research paper in this situation?

I want to learn more about graphs and trees for my independent research on improved graph visualization techniques. What are some good sources to learn, including, but not limited to, books, papers, YouTube, etc.?

Since I was young I have loved this type of mathematics, I learned about it as a C++ programmer

I have only come across Kenneth Rosen book, but I have wondered if there is a better book, I would like to learn more advanced concepts for personal projects

I am currently a year 2 CS student. I've been coding for 8 years now, but I'm realising that despite all that time, my general ability and knowledge level don't actually amount to much beyond being able to use libraries, APIs, frameworks etc.

Specifically, I'm really interested in low-level stuff and machine learning but I have no idea how to become good enough at it to actually start making meaningful contributions. It has become clear to me that my coursework is not going to be sufficient. What I mean by this is that if I take a compilers class or maybe a parallel computing class, that does not bring me up to a sufficient level where I can start making meaningful contributions to open source projects. I realise that I may be jumping the gun here (obviously a couple undergrad courses aren't going to get me anywhere close to the cutting edge) but all I'm asking here is direction for how to start.

I realise this is all very vague so maybe some examples of things that I am interested in (broadly at optimising the hell out of ML systems with low-level knowledge, parallel computing etc.) and wish to understand and be able to independently contribute to/produce:
How to write a fast Softmax kernel

Building Machine Learning Systems for a Trillion Trillion Floating Point Operations

I'm sorry if this is all vague, but I feel like I am at that point where I want to go deeper and really understand how some of this stuff works, but I have no idea where to turn to. I would be happy to clarify further. Thank you!

If an ASM expert (or team of experts) writes specifications for my team to re-write the code in OO languages, what level of detail and comprehensibility of the specs is realistically achievable?

We're talking abot hand-written assembly code with the owner's permission (in fact, they want us to rewrite it). No need to tell me it would be much harder for compiled code, and no need to tell me about licensing issues. And of course we're talking about programs that can be easily implemented in OOP (mostly file I/O and simple calculations), I certainly wouldn't attempt this with device drivers etc.

A brief survey of defeasible logic for automatic argumentation: https://gfrison.com/2024/12/01/defeasible-logic-automatic-argumentation

Basically the title. I have seen many people say they prefer Functional Programming, but I just can't understand why. I like implementing simple ideas functionally, but I feel projects with multiple moving parts are easier to build and scale when written using OOP techniques.