That's probably because propositional logic is decidable, so there is not as much motivation to find proofs when you can just grind it through a SAT solver.
^ that is the github repo I'm using for my paper, the tex is a bit of a mess but the haskell file there does the "substitution", we call it "intersection".
you might have expressions that are now defined and need to be expanded into different goals introduced by modus ponens, etc... I didn't exactly know where contradictions would come up
like
going from this step:
φ
ψ
ψ → (φ → (A → A))
φ → (A → A) M.P.
A → A M.P.
to this step:
A → χ
A → (χ → A)
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A) M.P.
A → A M.P.
there is a LOT going on
first you need to match ψ → (φ → (A → A)) with (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))
(which again, shares variable names which is confusing)
@Christopher I think your latest edit to the Sandbox seems better fitted to be a comment, so I'm rolling it back and would like to ask you to post it as a comment below the question
The one hiccup I would mention is that you need to screen out things like φ ∩ (φ → φ) where a variable is matched to an expression containing that variable.
In some nations there are recommendations or laws on how to form emergency corridors on streets that have multiple lanes per direction. (In the following we only consider the lanes going in the direction we are travelling.) These are the rules that hold in Germany:
If there is only one lane, e...
@H.PWiz I'm not siked about the metamath proof, but I do think that Metamath might be useful and it could help people who don't have very good ideas about the overall structure of their proof get a foothold.
Propositional calculus (also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic) is the branch of logic concerned with the study of propositions (whether they are true or false) that are formed by other propositions with the use of logical connectives. First-order logic extends propositional logic by allowing a proposition to be expressed as constructs such as "for every", "exists", "equality" and "membership", whereas in proposition logic, propositions are thought of as atoms.
== Explanation ==
Logical connectives are found...
Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Schemata, however, range over all propositions. It is common to represent propositional constants by A, B, and C, propositional variables by P, Q, and R, and schematic letters are often Greek letters, most often φ, ψ, and χ.
Is the program 32 or 64 bits?
Challenge is simple to explain: write the shortest code you need to determine supplied as a parameter is 32 or 64 bits on your platform.
If there is a different kind of bitness, you can also do for it, but is not mandatory.
What I really don't want is telling me y...
Just wanted to say that I've never posted an answer here, but I enjoy reading the challenges and answers. I like that this community is one of the few on SE that's consistently constructive. +1 to all of you.
@EriktheOutgolfer Maybe I will someday! I'm a software engineer, but I'm encouraged specifically not to write code like you guys usually do, for good reason! I'll have to put the effort into learning all of the usual tricks at some point. Probably start with Javascript, as that's mostly what I work with every day.
@maxathousand If you use JavaScript a lot, but don;t want to start golfing your professional code, you could take a look at Japt, which is a golfing language transpiled into JavaScript
Antigerrymandering
code-golf map set-partitions
From this question:
The United States has a unique love of gerrymandering––the deliberate manipulation of an electoral district to predict certain voting results. Just recently there was a gerrymandering case brought before the Supreme Court. ...
Decompile
popularity-contest compiler
Pick a language and call it language A. Pick a compiler for that language that translates it to another language, language B. Write a program or function in language A that receives a program in language B and prints/returns a program in language A that pro...
Is the program 32 or 64 bits?
Challenge is simple to explain: write the shortest code you need to determine an executable program supplied as a parameter is 32 or 64 bits.
If there is a different kind of bitness, you can also do for it, but is not mandatory.
What I really don't want is telling...
It's not too important anymore, but occasionally somebody needs to know.
Here is a simple golf: Taking no user input, tell me if the computer on which the code is run is on a 64-bit operating system, or a 32-bit operating system!
If the code is run on a 32-bit operating system, print "32", if t...
Up goes the number!
Given an integer N perform the following steps: (using 9 as an example).
Receive input N. (9)
Convert N from base10 to base2. (1001)
Increase every bit by 1. (2112)
Treat the result as base3 and convert it back to base10. (68)
Return/Output the result.
Input
May be rec...
Ordering by total stars is interesting. Alex is #1, and 4 of the 5 current mods are #2-6 (DJ is #11). All but 2 of the top 10 (Calvin and quartata) are TNB ROs. After typing all of that, I realize now that it's not that interesting and actually totally expected :P